RENAULT Etienne

Docteur
Équipe : MoVe
Date de départ : 31/12/2014
https://lip6.fr/Etienne.Renault
https://lip6.fr/Etienne.Renault

Direction de recherche : Fabrice KORDON

Co-encadrement : DURET-LUTZ Alexandre, POITRENAUD Denis

Contribution aux tests de vacuité pour le model checking explicite

L'approche automate pour le model checking de propriétés temporelles à temps linéaire est une technique classique de vérification formelle de systèmes concurrents. Un système, ainsi qu'une propriété qu'on souhaite y vérifier, sont modélisés sous forme d’omega-automates reconnaissant des mots infinis. Des manipulations de ces automates (produit synchronisé et test de vacuité) permettent d'établir si le système vérifie la propriété ou non.
Dans cette thèse nous nous focalisons sur un type particulier d'omega-automates qui permettent une représentation concise des propriétés d'équité faible: les automates de Büchi généralisés basés sur les transitions (Transition-based Generalized Büchi Automata).
Dans un premier temps, nous brossons un aperçu des algorithmes de vérification existant et nous en proposons de nouveaux traitant efficacement les automates généralisés forts. Dans un second temps, l'analyse des composantes fortement connexes de l'automate de la propriété nous a conduit à élaborer une décomposition de cet automate. Cette décomposition se focalise sur les automates multi-forces et permet une parallélisation naturelle des model-checkers. Enfin, nous avons proposé les premiers tests de vacuité parallèles pour les automates généralisés. De plus, tous ces tests sont lock-free à la différence de ceux de l’état de l’art. Toutes ces techniques ont ensuite été implémentées et évaluées sur un jeu de test conséquent.

Soutenance : 05/12/2014

Membres du jury :

Laure. Petrucci (Professeur à l'Université Paris 13) [rapporteur]
Francois Vernadat (Professeur à l'INSA toulouse) [rapporteur]
Jean-Michel. Couvreur (Professeur à l'Université d’Orléans)
Emmanuelle Encrenaz (Maitre de conférence à l'Université Paris 6)
Jaco van de Pol (Professeur à l'Université de Twente)
Alexandre Duret-Lutz (Maitre de conférence à l'EPITA)
D. Poitrenaud (Maitre de conférence à l'Université Paris 5)
Fabrice Kordon (Professeur à l'Université Paris 6)

Date de départ : 31/12/2014

1 Doctorante (Direction de recherche / Co-encadrement)

Publications 2010-2022

Mentions légales
Carte du site