RESPONSABLE : Didier BERT

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

LABORATOIRE ET EQUIPE : LSR - Équipe VASCO

TITRE : Analyse de comportement de systèmes B à l'aide de systèmes de transitions finis

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.

Dans les extensions actuelles de B, il est possible de décrire des systèmes d'évènements. Ces évènements peuvent se déclencher lorsque leur "garde" est vraie. Pour des systèmes complexes, il n'est pas facile de savoir quels évènements peuvent se déclencher dans un état donné, ni surtout quelle peut être l'évolution d'un système, c'est-à-dire l'enchaînement possible des évènements. Dans d'autres cas, l'utilisateur connaît a priori l'automate des transitions et il souhaite vérifier sur son système B qu'il en est bien ainsi. Pour étudier cela, l'équipe dispose d'un outil GeneSys (Générateur de Systèmes) qui permet de prouver qu'un évènement est déclenchable dans un état donné et qu'une transition vers tel autre état est possible. Cela donne un moyen de représenter les suites d'évènements à l'aide d'automates finis.

Dans ce projet, on demande d'étudier l'outil GeneSys sur plusieurs exemples de systèmes B. La conclusion de cette première partie sera une analyse de la pertinence de l'outil pour extraire des informations fines sur les transitions de ces systèmes. Dans un deuxième temps, on étudiera les outils attachés à la représentation du système de transition et on regardera quelles sont les extensions possibles en vue de la vérification des propriétés dynamiques (vivacité).

RESULTATS ATTENDUS :

Pratiques (réalisations) :
Etudes de cas de systèmes B. Analyse des caractéristiques et des performances de l'outil GeneSys.

Théoriques :
Etude des systèmes de transitions et preuve de propriétés dans ces systèmes. Expression des propriétés de vivacité en B et preuve de ces propriétés sur les systèmes de transitions.

Mots-clés:
Méthode B, spécification formelle, diagrammes de transitions, systèmes de transitions étiquetés.