Guillaume Brat, RIACS / NASA Ames, USA

Expériences en analyse statique de logiciels embarqués

Dans cette présentation, je vais décrire comment nous avons essayé d'appliquer des techniques d'analyse statique à des systèmes de vol embarqués de la NASA. Nos expériences avec des analyseurs commerciaux se sont revélées très décevantes. Nous avons donc dû concevoir notre propre analyseur, en nous servant de la théorie de l'interprétation abstraite. Cette présentation portera plus sur les expériences elles-mêmes que sur les détails théoriques des techniques des outils utilisés. J'essaierai de montrer, en me basant sur des études de cas réels, pourquoi l'analyse statique est importante pour la NASA.

Odile Laurent, Airbus

Le projet EICOSE

Le projet EICOSE (European Institute for Complex & Safety Critical Embedded Systems Engineering) devient officiellement le premier pôle d'innovation d'ARTEMIS (Advanced Research & Technology for EMbedded Intelligence and Systems), la plate-forme technologique européenne spécialisée dans le domaine des systèmes embarqués. Il inclut les pôles de compétitivité System@tic Paris-Region, Aerospace Valley, ainsi que le cluster allemand SafeTrans. Quatre des cinq groupes de travail du pôle Eicose sont particulièrement intéressants pour les chercheurs AFADL. A savoir : les Environnements de développement des systèmes embarqués critiques ; la réduction des coûts de développement de systèmes certifiables ; la conception pour la robustesse et la fiabilité ; l'interaction système pour les assistances homme-machine.

Jean-Raymond Abrial, ETH Zürich

Le B événementiel (Event-B) et son utilisation avec la plateforme Rodin

Le B événementiel a maintenant atteint sa maturité. L'exposé présente donc les principes et concepts de ce formalisme utilisé pour la modélisation de programmes séquentiels, distribués, concurrents ou parallèles ainsi que celle de systèmes complets incluant aussi bien un logiciel que son environnement. L'usage de ce formalisme est toujours basé, comme l'était le B "classique", sur la pratique du raffinement et de la preuve. Les outils de la plateforme Rodin permettent maintenant d'utiliser le B événementiel dans de bonnes conditions. On présentera donc aussi succintement cette plateforme ouverte et d'accès totalement libre.

Pierre Wolper, Université de Liège

Le calcul de fermetures par automates

Dans le cadre de la vérification de systèmes à espace d'états infini, les automates finis s'avèrent être une représentation for commode des ensembles d'états. En particulier, les ensembles de vecteurs d'entiers ou de réels se représentent très naturellement par des automates sur lesquels on peut directement appliquer des procédures de calcul. Dans ce contexte, nous considérons le problème de calculer l'enveloppe convexe d'un ensemble fini de vecteurs d'entiers à n dimensions représenté par une automate fini. La méthode consiste à calculer une séquence d'approximations de l'enveloppe convexe et à utiliser des techniques d'extrapolation pour obtenir la limite de cette séquence. La fermeture convexe peut alors être directement calculée à partir de cette limite sous la forme d'une représentation par automate de l'ensemble correspondant de vecteurs de réels. La technique est fort générale et a été implémentée avec succès.