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'automates reconnaissant des mots infinis (des ω-automates). Des manipulations de ces automates 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'ω-automates : les automates de Büchi généralisés basés sur les transitions (TGBA). Dans un premier temps nous revisitons les deux principales étapes de l'approche : la traduction de formules de logique temporelle à temps linéaire en TGBA et le test de vacuité (emptiness check) d'un TGBA. Pour chacune, nous proposons des améliorations des algorithmes existants, et comparons ces algorithmes pour montrer l'intérêt des TGBA.
Dans un deuxième temps, nous proposons deux variations du test de vacuité. L'une peut être utilisée avec certains algorithmes qui réduisent l'automate représentant le système en regroupant ses états de façon symbolique. Elle utilise des tests d'inclusion entre ces regroupements d'états pour guider la construction à la volée de l'automate. L'autre est une généralisation aux automates de Streett (à nouveau basés sur les transitions); elle permet de prendre en compte des hypothèses d'équité forte lors de la vérification.
| Mot clefs: | vérification formelle, model checking, ω-automates, automates de Büchi, logique temporelle, LTL, test de vacuité, algorithmes |
|---|
The automata theoretic approach to model checking linear-time temporal properties is a classical verification technique for concurrent systems. Both the system and the property to verify are expressed as automata on infinite words (ω-automata). Some operations on these automata establish whether the property holds in the system.
In this thesis we focus on a kind of ω-automata called Transition-based Generalized Büchi Automata (TGBA). We start by revisiting the main two steps of the approach: the translation of linear-time temporal logic formulae into TGBA, and the emptiness check of TGBA. For each of these steps, we offer improvements to existing algorithms, and compare them to show the benefits of using TGBA.
We then introduce two variants of the emptiness check algorithm. The first one can be combined with algorithms that aim at reducing the automaton which represents the system by gathering some of its states symbolically. The new emptiness check uses inclusion checks between these symbolic sets of states to drive the on-the-fly construction of the automaton. The second variant is a generalization to (transition-based) Streett automata; it enables the verification of properties under strong fairness assumptions.
| Keywords: | formal verification, model checking, ω-automata, Büchi automata, temporal logic, LTL, emptiness check, algorithms |
|---|
La soutenance a eu lieu au LIP6 le mardi 10 juillet 2007 à 14h30, salle 549, site Passy-Kennedy.
| Ahmed Bouajjani | Professeur à l'Université Paris 7 | Rapporteur |
| François Vernadat | Professeur à l'INSA de Toulouse | Rapporteur |
| Jean-Michel Couvreur | Professeur à l'Université d'Orléans | Examinateur |
| Claude Girault | Professeur émérite à l'Université Paris 6 | Examinateur |
| Alain Griffault | Maître de conférences à l'Université Bordeaux 1 | Examinateur |
| Serge Haddad | Professeur à l'Université Paris-Dauphine | Examinateur |
| Fabrice Kordon | Professeur à l'Université Paris 6 | Directeur de thèse |
| Denis Poitrenaud | Maître de conférences à l'Université Paris 5 | Encadrant |