Titre :

Maîtrise de l'explosion d'états dans la vérification de systèmes à architecture complexe

Résumé :

La vérification formelle est indispensable pour assurer la fiabilité des applications industrielles ayant une architecture complexe (protocoles de communication, systèmes répartis, etc.). La méthode de vérification basée sur les modèles (model-checking) est particulièrement attractive en pratique, permettant une détection automatique et efficace des erreurs dès le début du processus de conception. Cette méthode consiste à spécifier l'architecture et le comportement du système en utilisant un langage de haut niveau, à traduire cette spécification vers un modèle système de transitions (graphe d'états ou automate) et à vérifier sur ce modèle les propriétés attendues du système (exprimées en logique temporelle) au moyen d'algorithmes spécifiques.

La vérification des systèmes de grande taille, comportant de nombreux processus parallèles et des types de données complexes, est confrontée au problème de l'explosion d'états : dans certains cas, le nombre d'états du modèle peut dépasser la mémoire des machines disponibles. Différentes approches ont été proposées pour combattre l'explosion d'états :

• La vérification compositionnelle (travaux de R. Cleaveland, H. R. Andersen, C. Stirling) permet de décider la satisfaction d'une propriété sur un système à structure hiérarchique en décidant la satisfaction de plusieurs autres propriétés sur chacune des composantes du système. Ceci permet d'effectuer la vérification en construisant uniquement les modèles des composantes du système, sans construire le modèle du système complet.



• Les ordres partiels (travaux d'A. Valmari, P. Godefroid, D. Peled, F. Vernadat) évitent la génération de certains entrelacements d'actions produits par des transitions causalement indépendantes (par exemple, des transitions appartenant à des processus parallèles qui ne se synchronisent pas). De cette manière, certaines classes de propriétés peuvent être vérifiées en explorant une partie relativement réduite du modèle.



• Les symétries (travaux de N. Ip, D. Dill, L. Bougé) exploitent la répétition de structures similaires souvent rencontrée dans les systèmes répartis (par exemple, la présence de plusieurs processus parallèles identiques qui ne différent que par les valeurs de leurs paramètres). Cette technique permet d'éviter la génération de certaines parties du modèle qui seraient obtenues par symétrie.

Jusqu'à présent, ces techniques pour combattre l'explosion d'états ont été appliquées uniquement pour des modèles ou langages simples et n'ont été que très peu implémentées. En outre, ces techniques ont été employées uniquement de manière séparée, aucune tentative n'ayant été effectuée pour leur intégration.

L'objectif de cette thèse est d'étudier et de mettre en oeuvre la combinaison de ces techniques pour des langages de spécification capables de décrire des applications industrielles ayant des architectures logicielles complexes. Ces langages, inspirés des calculs de processus et enrichis avec des constructions de haut niveau permettant de décrire des architectures hiérarchiques complexes, sont conçus de manière à posséder à la fois une sémantique rigoureuse, adaptée à la vérification formelle, et une syntaxe conviviale, adaptée à l'utilisation industrielle.

Le travail devra s'appuyer sur un modèle sémantique intermédiaire, suffisamment expressif pour représenter les concepts essentiels de ces langages et permettant une compilation et une exécution efficace. Sur ce modèle, il faudra étudier l'application combinée des techniques d'optimisation, afin d'améliorer les performances de la vérification.

Les algorithmes proposés seront mis en oeuvre dans la boîte à outils CADP, l'environnement de spécification et vérification d'applications critiques développé au sein du projet VASY.

Niveau de compétence requis :

• Titulaire d'un diplôme de DEA en informatique



• Expérience souhaitée dans le domaine des méthodes formelles et de la vérification

Date prévisible de début de la thèse : 1er décembre 2001

Durée du contrat de financement : 3 ans

Pour tous renseignements sur l'emploi proposé, contacter :

Radu Mateescu
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
38330 MONTBONNOT SAINT-MARTIN
Tel : 04 76 61 52 83
Fax : 04 76 61 52 52
E-mail : Radu.Mateescu@inria.fr

Composition du dossier de candidature :

• lettre de candidature et de motivation



• curriculum vitae comprenant les études, ainsi que les réalisations logicielles effectuées



• les éventuelles publications



• les éventuelles références ou lettres de recommandation

Back to the VASY Home Page