RESPONSABLE : Didier BERT

TEL : 04 76 82 72 16
ADRESSE ELECTRONIQUE : Didier.Bert@imag.fr< /A>

LABORATOIRE ET EQUIPE : LSR - Équipe VASCO

TITRE : Transformation de développements B

RESUME :
Dans le domaine des systèmes critiques, il est important de vérifier la correction du logiciel et de valider certaines propriétés importantes. Pour réaliser cela, on a recours à des langages qui permettent de spécifier les comportements à des niveaux assez abstraits et par un processus de raffinement, on produit du code prouvé correct par rapport aux spécifications. Certains processus de certification des produits logiciels demandent explicitement l'utilisation de telles approches. La méthode B fait partie des méthodes les plus utilisées dans ce domaine (ligne de métro automatique MÉTÉOR à Paris). Les outils liés à la méthode (AtelierB) permettent de développer des applications depuis les spécifications jusqu'au code exécutable par un processus de raffinements successifs.

L'équipe a développé une Boîte à Outils pour B (BoB) qui permet de représenter les composants B sous une forme interne en Java. Le but du stage est de construire, au-dessus de cette boîte à outils, une couche de logiciels qui permette de générer automatiquement de nouveaux développements à partir des anciens. Certaines transformations ont déjà été étudiées théoriquement (aplatissement de raffinements, génération de machines à partir de raffinements, etc.). Le stage permettra d'implémenter en Java les algorithmes décrits dans ces articles. Il sera demandé également d'étudier d'autres transformations, de les décrire et de les implanter dans cette couche de logiciel. Un point particulièrement intéressant sera de voir comment les lemmes qui assurent la correction des développements sont aussi transformés et comment les preuves de correction des nouveaux développements peuvent être construites à partir des preuves des anciens développements.

RESULTATS ATTENDUS :

Pratiques (réalisations) :
Construction de la couche de logiciel en Java pour transformer des développements écrits en B. Introduction de fonctionnalités nouvelles dans la boîte à outils BoB.

Théoriques :
Etude des relations entre composants B. Etude des transformations de développements. Validation automatique des développements engendrés par l'outil.

Mots-clés:
Méthode B, spécification formelle, processus de raffinement, composants.