next up previous
Next: Sujet : Extensions de Up: Sujets de thèse autour Previous: Sujet : Modélisation et

Sujet : Intégration des techniques de preuve de théorèmes et de vérification symbolique pour la preuve de circuits séquentiels

 

Fiche signalétique

Responsable Antoine Rauzy 05 56 84 60 83 Antoine.Rauzy@labri.u-bordeaux.fr
Collaborateur David Sherman 05 56 84 69 22 David.Sherman@labri.u-bordeaux.fr
Equipe MVTsi
Titre
Intégration des techniques de preuve de théorèmes et de vérification symbolique pour la preuve de circuits séquentiels.
Catégorie Théorique et expérimentale
Position/AltaRica Outil satellite
Moyen terme
Financement Bourse de thèse BDI ou MENRT

Présentation du sujet

Contexte
Le comportement de nombreux systèmes industriels peut être modélisé par un automate booléen avec entrée-sorties (une machine de Mealy). La vérification de propriétés sur ce type de modèles se fait jusqu'à présent par parcours de l'espace des états accessibles de l'automate. L'introduction de techniques de parcours symbolique (utilisant un codage par diagrammes binaires de décision, BDD) a permis des progrès considérables dans la taille des systèmes traitables. Toutefois, de nombreux systèmes réels restent hors de portée, en raison de l'explosion combinatoire du nombre d'états à explorer, ou de la taille des BDD codant ces états. Pour aller plus loin, une technique prometteuse consiste à décomposer les automates étudiés suivant la propriété à vérifier. Or, il faut prouver formellement que ce type de décomposition est correcte.

Travail demandé
Le sujet de la thèse est donc d'étudier l'intégration d'assistants de preuve du type PVS et d'outils de vérification symbolique du type SMV, en partant des travaux déjà effectués sur ce thème.

Environnement
La thèse s'appuiera sur plusieurs exemples de systèmes industriels qui sont d'ores et déjà disponibles (au LaBRI) et font l'objet de collaboration entre le LaBRI et divers partenaires industriels (CEA, Aerospatiale).


next up previous
Next: Sujet : Extensions de Up: Sujets de thèse autour Previous: Sujet : Modélisation et

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