Proposition de Travaux d'Etude et de Recherche
Maîtrise 2000-2001
Sujet :
Exploration partielle d'automates
Responsables :
Paul Gastin (http://www.liafa.jussieu.fr/~gastin),
Mihaela Sighireanu (http://www.liafa.jussieu.fr/~sighirea)
Nature du stage :
Programmation (au choix : C, C++, Java, Perl, ou HTML).
Nombre d'étudiants dans le groupe :
de 1 à 3.
Description du sujet :
La complexité des systèmes informatiques actuels, particulièrement dans le cadre des systèmes réactifs, des systèmes concurrents ou des systèmes temps réel, rend extrêmement difficile le développement de systèmes fiables. Le crash d'Ariane 5 illustre les conséquences extrêmes que peuvent avoir les erreurs dans les systèmes informatiques. Dans ces conditions, la vérification formelle des systèmes informatiques est de première importance. Pour faciliter cette tâche, des outils de vérification ont été développés ces dernières années.
La plupart de ces outils génèrent un automate d'états fini qui représente le comportement du système à vérifier. Plusieurs outils de visualisation complète d'automates existent. Mais, quand l'automate est très gros, la visualisation complète de l'automate est trop chargée pour être utilisée pour l'exploration de l'automate. C'est pourquoi il serait utile de pouvoir explorer partiellement l'automate à partir d'un état.
Le but du stage est de proposer et de programmer un outil qui permet l'explorations partielle des automates. Les automates sont données sous forme d'un fichier texte, dans un format particulier. Initialement, l'outil doit afficher la liste de tous de états. L'utilisateur peut sélectionner un état et demander l'explorations de l'automate à partir de cet état, sur une profondeur donnée. Le programme doit construire le sous-automate correspondant à cette exploration (par des filtrages intelligents sur le fichier texte) et donner cet automate aux outils de visualisation classique.
On utilisera le package Graphics développé à AT&T pour la visualisation d'automates:
http://www.research.att.com/sw/tools/graphviz/
Connaissances préalables souhaitées :
- Programmation,
- Compilation (essentiellement l'analyse syntaxique),
- Automates.
Resultats :
- Ce sujet a ete choisi en mai 2001 par Guillaume Journaux et Gwenole Tallec et a donne lieu a une extension de l'outil GraphViz avec le module exploration.lefty.
This project has been done in May 2001 by Guillaume Jounaux and Gwenole Tallec. They proposed an extension of the GraphViz tool with the module exploration.lefty.