next up previous
Next: Sujet : Techniques de Up: Sujets de thèse autour Previous: Sujet : Intégration des

Sujet : Extensions de structures de données partagées pour la vérification de systèmes complexes

 

Fiche signalétique

Responsable André Arnold 05 56 84 60 94 Andre.Arnold@labri.u-bordeaux.fr
Collaborateurs David Sherman 05 56 84 69 22 David.Sherman@labri.u-bordeaux.fr
Jean-Michel Couvreur 05 56 84 69 34 Jean-Michel.Couvreur@labri.u-bordeaux.fr
Equipe MVTsi
Titre
Extensions de structures de données partagées pour la vérification de systèmes complexes.
Catégorie Théorique et expérimentale
Position/AltaRica Outil satellite
Moyen terme
Financement Bourse de thèse MENRT

Présentation du sujet

Contexte
Le vérification de systèmes complexes s'appuie de plus en plus sur des techniques et outils de caractère mixte, intégrant de différents formalismes et moyens de mise en oeuvre. De par les problèmes d'explosion combinatoire engendrés par les systèmes complexes, ces différentes techniques doivent utiliser des structures de données représentant de façon très compacte les systèmes à étudier. Les diagrammes binaires de recherche (BDD) et arbres partagés en sont des exemples répandus.

Travail demandé
Le sujet de la thèse est d'étudier et de mettre en uvre sur ces structures partagées un certain nombre d'opérations élémentaires (ensemblistes, quantifications, points fixes) et de bâtir sur elles un vérificateur pour des logiques plus puissantes que les logiques temporelles. Une réflexion sur les relations entre le mu-calcul et la logique temporelle permettra l'étude du pouvoir d'expression de ces logiques.

Environnement
La thèse s'appuiera sur les systèmes existants Mec et Toupie et leur intégration dans un nouvel outil de vérification basé sur le système Factotum. L'outil ainsi réalisé se trouvera en aval du projet AltaRica, et exploitera des techniques issus du projet Clovis.


next up previous
Next: Sujet : Techniques de Up: Sujets de thèse autour Previous: Sujet : Intégration des

Equipe Modélisation, Vérification et Test des systèmes informatisés
Fri May 15 10:32:44 CEST 1998