RESPONSABLE : Didier BERT, Marie-Laure POTET

TEL : 04 76 82 72 16, 04 76 82 72 69
ADRESSE ELECTRONIQUE : Didier.Bert@imag.fr< /A>, Marie-Laure.Potet@imag.fr

LABORATOIRE ET EQUIPE : LSR - Équipe VASCO

TITRE : Amélioration des performances d'un générateur de lemmes pour vérifier la correction des logiciels

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. Un composant essentiel de l'AtelierB est le générateur des lemmes qui assurent la correction des spécifications et la validité des propriétés énoncées.

Ce générateur de lemmes, appelé aussi Générateur d'Obligations de Preuve (GOP) se base sur la théorie du calcul des "plus-faibles préconditions". Cependant, la mise en oeuvre directe de cette théorie conduit à des programmes d'une certaine inefficacité. Le problème d'efficacité est crucial pour des applications industrielles qui produisent plusieurs dizaines de milliers de lemmes. Le sujet du DEA consiste donc à étudier le principe du GOP, à identifier les causes potentielles d'inefficacité et à proposer et à mettre au point des techniques pour y remédier. Pour réaliser ce travail, l'étudiant pourra disposer de l'AtelierB ainsi que d'un outil prototype développé dans l'équipe. L'outil prototype permettra de tester les algorithmes d'optimisation du GOP. L'étudiant sera en contact avec la société ClearSy qui maintient et qui commercialise l'AtelierB.

Outre ce travail d'optimisation du GOP, il sera possible d'étudier l'intégration d'un outil de vérification de bonne définition des expressions, ainsi que la visualisation des liens entre les lemmes engendrés et le texte initial des spécifications (traçabilité).

RESULTATS ATTENDUS :

Pratiques (réalisations) :
Amélioration des performances du programme de génération des obligations de preuve.

Théoriques :
Spécification du GOP et justification des optimisations (correction et gains).

Mots-clés:
Méthode B, spécification formelle, logique du 1er ordre, démonstration.