Laïka Moussa, étudiante en DESS Développement des Logiciels Sûrs à Paris VI et au CNAM, a réalisé son stage de fin d’étude en collaboration avec le CETIC et les FUNDP. Cet article présente son rapport et présentera sous peu l’outil qu’elle a codé.
Expertises:
Ingénierie des systèmes IT complexes ⊕
B est une méthode de développement de programmes (et de plus en plus de systèmes) basée sur une approche de "correction par construction" intégrant la notion de raffinement successifs, depuis des spécifications abstraites, proches des exigences, jusqu’à des spécifications opérationnelles desquelles du code peut directement être généré.
L’approche prônée par les principaux outils B (Atelier B, B Toolkit) est axée sur la vérification et basée sur des outils de preuves formelles. Ceux-ci nécessitent une expertise certaine et ne sont pas donc pas à la portée des utilisateurs industriels moyens, ni des étudiants en début de cursus.
Dans le présent travail, l’idée était de mettre en oeuvre des techniques de model-checking qui ne permettent d’obtenir l’assurance de la correction que pour des domaines finis mais qui, en contrepartie, sont automatiques et fournissent des contre-exemples permettant de découvrir les erreurs et d’aider à les corriger. L’utilisation envisagée est principalement de nature pédagogique.
Concrètement, l’exploration de l’espace d’état a été mise en oeuvre en utilisant des techniques de résolution de contraintes et mise en oeuvre sur la plate-forme MOZART.
Le rapport de stage retrace tout le processus amenant à la réalisation de l’outil : sujet, cahier des charges (inclus en annexe), conception détaillée des algorithmes et mise en oeuvre sur la plate-forme OZ.
Voici également la présentation passée lors de la soutenance de stage était claire (environ 35 minutes).
Enfin, l’outil, nommé VICS, a été libéré et est distribué sous licence GPL. Il est disponible sur SourceForge.
Voir en ligne : VICS sur SourceForge