Index

Au sein de laboratoire de l'Université de Franche Comté

Au sein de l’équipe Techniques Formelles et à Contraintes du Laboratoire d’Informatique de l’Université de Franche-Comté ma problématique de recherche consistait à étudier et définir des techniques permettant de diminuer l’explosion combinatoire de l’algorithme de vérification de propriétés de Logique Temporelle Linéaire sur des spécifications de systèmes réactifs.

Présentation des travaux

Le thème de recherche dans lequel s'est inscrit mon travail de thèse est intitulé Génie logiciel et Intelligence Artificielle. Il s'inscrit dans le projet Spécification formelle, validation et vérification de logiciels dont le responsable J. Julliand est aussi mon directeur de thèse. L'objectif de ce projet est de développer un environnement de conception formelle de logiciel ,utilisant des techniques de vérification hétérogène. On attend de la coopération de ces techniques la possibilité de vérifier l'ensemble des propriétés que doit vérifier le système. Le but est donc d'intégrer à la méthode B des outils de vérification de spécification en Logique Temporelle Linéaire. La vérification de propriétés LTL conciste à vérifier la consistance de deux énoncés :

• une spécification descriptive formée d'un modèle de données abstrait, de propriétés invariantes décrits en B et de propriétés dynamiques décrites en logique temporelle linéaire,
• une spécification opérationnelle formée d'un ensemble d'opérations faisant évoluer le système. Celles-ci sont décrites formellement en B par des événements sous forme condition-action.

La consistance des propriétés invariantes est vérifiée par le prouveur de la méthode B. Celle des propriétés temporelles est vérifiée par les méthodes d'exploration algorithmique de modèles (model checking) adaptées au niveau d'abstraction du modèle de données abstrait. Nous développons un model-checker travaillant sur une spécification B. Le model checker profite du niveau d'abstraction du langage B pour réduire la compléxité du graphe d'accessibilité. En particulier pour réussir cela deux techniques sont étudiées :

•  l'abstraction de certaines variables
•  le raffinement des spécifiations.

 Mes travaux de recherche s'inscrivent dans le cadre du projet spécification formelle, Validation et vérification de logiciels au sein de l'équipe Techniques formelles et à Contraintes du Laboratoire d'Informatique de l'Université de Franche-Comté qui vise l'extension de la méthode B par de la Logique Temporelle Linéaire. 

Ma contribution à ce projet a consisté en premier lieu en la réalisation d'un état de l'art sur les différentes approches permettant de combattre l'explosion combinatoire du nombre d'états (principale limite du model-checking). 

Une fois cette tâche réalisée, nous avons entrepris de définir des techniques nouvelles pour combattre ce problème. Deux technique ont été étudiées : 

•  la compression des états 
•  l'utilisant la Programmation en Logique avec Contrainte sur les Ensembles . 

La compression des états a été réalisée en utilisant les chaînes de collisions de la table de hachage du model-checker.  

La deuxième voie peut être classée comme une technique d'interprétation abstraite. En effet, l'utilisation des contraintes ensemblistes a pour effet de réaliser une abstraction sur le modèle, puisque l'on réduit le nombre d'états en regroupant ceux qui ont des caractéristiques communes. Les meta-états seront traités de façon symbolique grâce à la technologie des contraintes.. 

Résultats

La technique de compression mémoire a été implantée dans SPIN outils développé par G. Holzmann des laboratoires At&t. Nous avons réalisé quelques évaluations de performances que nous présentons dans l'articles 'Difference compression in SPIN' et dans ma thèse.

L'implantation d'un model-checker travaillant sur des spécifications réalisées en langage B a permis de valider nos idées. Ce model-checker est écrit en C++ avec une interface en langage JAVA. Nous avons réalisé des évaluations de performances sur ce model-checker que je présente dans ma thèse. 

Participation à la formation par la recherche

Participation à l’encadrement d’un étudiant de DEA ayant pour but la réalisation d’un outil permettant la décomposition de l’espace d’états accessibles en modules en utilisant le raffinement,

Réalisation de Travaux Pratiques d’introduction à l’utilisation de l’outil SPIN et de l’atelier B.

Au sein de France Télécom / ORANGE

Je travaille actuellement à France Télécom R&D toujours dans le domaine de la recherche en méthodes formelles. Cependant, mes recherches me font explorer des pistes allant du test au diagnostic.

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