Index

Ma thèse « Vérification de systèmes d’événements B par model-checking PLTL - Contribution à la réduction de l’explosion combinatoire en utilisant de la résolution de contraintes ensemblistes » a été soutenue le 08 Décembre 2000 à l’Université de Franche-Comté et a été réalisée sous la direction du Professeur Jacques Julliand et du Maître de Conférences Hassan Mountassir.

Le manuscrit de ma thèse est disponible ici :

•  en pdf 1,35 Mo

Membres du jury

•  Pr. J. JULLIAND (LIFC, Université de Franche-Comté, Directeur),
•  Pr. H. HABRIAS (IRIN, Université de Nantes, Rapporteur),
•  Pr. D. MERY, (LORIA, Université de Nancy 1, Rapporteur),
•  Pr. B. LEGEARD (LIFC, Université de Franche-Comté, Président du Jury),
•  Pr. F. BELLEGARDE (LIFC, Université de Franche-Comté),
•  MdC H. MOUNTASSIR (LIFC, Université de Franche-Comté),
•  CR-CNRS P. SCHNOEBELEN (LSV, Ecole Normale Supérieur Cachan)

Résumé

Les travaux de cette thèse portent sur la vérification de spécifications formelles par model-checking de propriétés dynamiques exprimées en Logique Temporelle Linéaire. La principale limite de cette technique est connue sous le nom d’explosion combinatoire du nombre d’états. Les travaux présentés dans ce manuscrit visent à combattre cette explosion combinatoire afin de rendre possible la vérification de spécifications de taille industrielle.

Nous définissons deux approches possibles l’une fondée sur l’utilisation d’une technique de compression spécifique et l’autre sur une technique d’abstraction automatique réalisée par le biais de l’utilisation de programmation en logique avec contrainte.

Cette recherche nous a conduit à réaliser une implantation de chacune de ces techniques. L’implantation de la technique de compression a été réalisée dans SPIN, qui est un model-checker connu dans le domaine des systèmes communicants. Cette technique de compression réalise une partition des vecteurs d’état pour améliorer le taux de compression. La partition est réalisée au niveau de la table de ‘hashing’ habituellement utilisée pour accélérer les recherches dans l’espace d’états.

L’implantation de la technique basée sur la résolution de contraintes ensemblistes, nous a conduit à réaliser un model-checker pour le langage B. Nous utilisons un solveur ensembliste, appelé CLPS-B, développé au sein du laboratoire pour obtenir une représentation abstraite de l’espace d’états généré par le model-checker. Nous obtenons de cette façon une diminution significative du nombre d’états à représenter.

Enfin, ces deux implantations ont permis d’évaluer nos solutions. Ces évaluations ont été réalisées sur différents problèmes, dont certains de taille industrielle, et nous avons pu ainsi montrer l’intérêt et la pertinence de chacune de nos deux approches.

Mots clés 

spécification formelle, vérification, Logique Temporelle Linéaire, model-checking, explosion combinatoire, abstraction, programmation en logique avec contraintes ensemblistes, compression.

Cette page a été mise à jour le 20/08/09.