Proposition de projet de Master 2 Recherche

2005/2006

Titre

Combinaison de techniques de vérification compositionnelle pour les systèmes embarqués

Domaines de recherche

Vérification formelle - Systèmes embarqués

Sujet

Le projet de Master 2 Recherche (ex-DEA) proposé s'effectuera à l'INRIA Rhône-Alpes, au sein des équipes VASY et POP ART, qui développent des méthodes formelles et des outils logiciels pour produire des systèmes fiables et assister le flot de conception de systèmes embarqués sûrs.

Le projet de Master porte sur la vérification formelle des systèmes embarqués comprenant plusieurs composants qui s'exécutent en parallèle et interagissent. Dans l'approche que nous considérons, le système à vérifier est modélisé formellement dans le modèle Prometheus, qui permet trois niveaux de description :

• modèle des composants
• modèle des interactions entre composants
• modèle d'exécution qui établit des priorités entre les interactions possibles

Il s'agit en particulier d'étudier et de combiner des méthodes de vérification compositionnelle, qui consistent à décomposer la vérification du système complet en vérifications plus simples sur chacun de ses composants.

L'objectif est de combiner de manière intelligente des techniques complémentaires de vérification compositionnelle :

• la vérification de conditions suffisantes sur les composants, le modèle d'interaction et le modèle d'exécution permet de garantir par construction des propriétés de vivacité, d'atteignabilité et/ou de déterminisme ; lorsque les conditions suffisantes ne sont pas satisfaites dans le modèle initial, il est possible de synthétiser des contraintes supplémentaires qui garantissent les propriétés souhaitées ; cette technique a été implémentée dans l'outil Prometheus développé par POP ART;
• la vérification compositionnelle énumérative consiste à générer un graphe d'états pour chaque composant, à abstraire et réduire ces graphes, puis à les recomposer pour obtenir le graphe d'états réduit du système complet ; la boîte à outils CADP développée par VASY comprend plusieurs formats et outils permettant la vérification compositionnelle, notamment le format BCG permettant de représenter des graphes d'états de manière compacte, l'outil Exp.Open 2.0 permettant de composer les graphes d'états en parallèle, des outils de réduction et d'abstraction de graphes d'états, des model checkers, etc.

On pourra envisager plusireurs manières de combiner ces techniques, comme par exemple :

• l'utilisation de CADP pour vérifier certains types de propriétés non prises en compte par Prometheus (sûreté, équivalence de comportement, etc.)
• l'utilisation de CADP par Prometheus pour affiner la vérification des composants
• l'exploitation par CADP des résultats de Prometheus, lui permettant d'appliquer des abstractions plus fortes sur les graphes d'états des composants
• etc.

Pour cela, une traduction automatique du modèle Prometheus vers les formats disponibles dans la boîte à outils CADP sera nécessaire.

Ce projet de Master abordera donc les thèmes suivants :

• Tour d'horizon des techniques de vérification formelle
• Etude de l'état de l'art dans le domaine de la vérification compositionnelle
• Compréhension des outils Prometheus et CADP
• Compilation du modèle des composants de Prometheus vers les graphes d'états BCG
• Compilation du modèle d'interaction de Prometheus vers le format Exp.Open 2.0
• Extension de Exp.Open 2.0 pour prendre en compte les priorités entre interactions
• Proposition d'une méthodologie de vérification qui s'appuie sur la combinaison des outils disponibles et de nouveaux outils prototypes éventuels
• Application sur une étude de cas industrielle en micro-électronique ou en bioinformatique.

En fonction de l'intérêt des résultats obtenus, ce projet pourra déboucher sur une thèse au sein des équipes VASY ou POP ART.

Références

• G. Goessler et J. Sifakis, "Composition for Component-Based Modeling", Science of Computer Programming 55(1-3), 2005.
• An overview of CADP 2001
• Outils de vérification CADP, http://cadp.inria.fr

Contacts

Pour plus d'informations concernant ce projet, contacter de préférence par courrier électronique (adresses au format Prenom.Nom@inria.fr) les deux personnes suivantes :

• Gregor Goessler (POP ART), 04 76 61 54 20
• Frédéric Lang (VASY), 04 76 61 55 11