Soutenance d'habilitation à diriger des recherches de Radu Mateescu

Radu MATEESCU soutiendra le 28 septembre 2007 à 11 h
au Grand Amphithéâtre de l'INRIA Rhône-Alpes
655, avenue de l'Europe 38330 Montbonnot Saint Martin

une habilitation à diriger des recherches de l'Institut National Polytechnique de Grenoble,
intitulée :

"Composants génériques pour l'analyse des systèmes de transitions"

COMPOSITION DU JURY :

• M. Jean-Pierre VERJUS, Directeur Général Adjoint de l'INRIA (président du jury)
  
• M. Nicolas HALBWACHS, directeur de recherche CNRS (rapporteur)
  
• M. Holger HERMANNS, professeur à l'Université de la Sarre (rapporteur)
  
• M. Philippe SCHNOEBELEN, directeur de recherche CNRS (rapporteur)
  
• M. Jean-Marie BILBAULT, professeur à l'Université de Bourgogne (examinateur)
  
• M. Bernard ESPIAU, directeur de recherche INRIA (examinateur)
  
• M. Hubert GARAVEL, directeur de recherche INRIA (examinateur)
  

La soutenance sera naturellement suivie d'un pot, à côté de l'amphithéâtre, auquel vous êtes tous cordialement invités.

RÉSUMÉ :

La construction d'outils de vérification efficaces et robustes est une tâche complexe, qui requiert des investissements importants en termes de recherche théorique, de génie logiciel, d'expérimentation et de mise au point. Cette tâche peut être considérablement simplifiée en adoptant des architectures modulaires, qui facilitent le développement, l'optimisation et le test séparé des modules, ainsi que leur réutilisation dans des contextes différents.

La première partie de ce document définit un ensemble de composants génériques pour la construction d'outils de vérification à la volée, qui explorent de manière incrémentale les systèmes de transitions étiquetées (STEs) modélisant le comportement des systèmes à vérifier. Deux types de composants sont proposés : les solveurs effectuent la résolution locale des systèmes d'équations booléennes (SEBs) suivant plusieurs stratégies (parcours en profondeur, en largeur, etc.) et produisent des diagnostics (exemples et contre-exemples) expliquant la valeur de vérité des variables ; les réducteurs identifient à la volée les états des STEs qui sont équivalents modulo différentes relations (tau-compression, tau-fermeture, tau-confluence) afin de diminuer la taille des STEs tout en préservant des propriétés utiles. Les solveurs et les réducteurs ont été développés comme bibliothèques (CAESAR_SOLVE, respectivement CAESAR_EDGELIST) au moyen de l'environnement générique OPEN/CAESAR pour la manipulation de graphes situé au centre de la boîte à outils CADP, ce qui assure l'indépendance de ces composants par rapport aux langages utilisés pour décrire les systèmes à vérifier.

La deuxième partie du document présente trois applications de ces composants dans le domaine de la vérification à la volée, chacune étant implémentée au coeur d'un ou plusieurs outils intégrés à CADP : la génération séquentielle et distribuée de STEs, assortie de réductions à la volée (contribution aux outils REDUCTOR 5.0, DISTRIBUTOR 3.0 et BCG_MERGE 3.0) ; la vérification par évaluation de propriétés temporelles, exprimées comme formules du mu-calcul modal étendu avec des données, des expressions régulières et des opérateurs non-standard (outils EVALUATOR 3.x et 4.0) ; et la vérification par comparaison de STEs modulo sept relations d'équivalence largement utilisées (outil BISIMULATOR). L'architecture de chaque outil est décrite en soulignant ses différents composants constituants et leur interconnexion. Les performances sont également illustrées par des données expérimentales obtenues en analysant des systèmes de grande taille.

MOTS-CLÉS :

bisimulation, equivalence checking, logique temporelle, model checking, mu-calcul modal, réduction par ordres partiels, spécification, système d'équations booléennes, système de transitions étiquetées, vérification à la volée

TITLE:

Generic Components for the Analysis of Transition Systems

ABSTRACT:

The construction of efficient and robust verification tools is a complex task that requires an important spending in terms of theoretical research, software engineering, experimenting and debugging. This task can be significantly simplified by adopting modular architectures, which facilitate the separate development, optimisation, and testing of modules, as well as their reuse in various contexts.

The first part of this document defines a set of generic components for bulding on-the-fly verification tools, which explore incrementally the labelled transition systems (LTSs) modelling the behaviour of the systems under analysis. Two types of components are proposed: the solvers perform the local resolution of boolean equation systems (BESs) along several strategies (depth-first search, breadth-first search, etc.) and produce diagnostics (examples and counterexamples) explaining the truth value of the variables; the reductors identify on-the-fly those LTS states equivalent modulo various relations (tau-compression, tau-closure, tau-confluence) in order to decrease the LTS size but still preserve useful properties. Solvers and reductors were developed as software libraries (CAESAR_SOLVE and CAESAR_EDGELIST, respectively) by using the generic OPEN/CAESAR environment for graph manipulation placed at the center of the CADP verification toolbox, which ensures the independence of these components w.r.t. the languages used to describe the systems under analysis.

The second part of the document presents three applications of these components in the field of on-the-fly verification, each of them being implemented at the heart of one or several tools integrated into CADP: sequential and distributed LTS generation, enhanced with on-the-fly reductions (contributions to the REDUCTOR 5.0, DISTRIBUTOR 3.0, and BCGMERGE 3.0 tools); model checking of temporal properties expressed as formulas of modal mu-calculus extended with data, regular expressions, and non-standard operators (EVALUATOR 3.x and 4.0 tools); and equivalence checking by comparing LTSs modulo seven widely-used equivalence relations (BISIMULATOR tool). The architecture of each tool is described by underlining its various components and their interconnection. The performances are also illustrated by experimental data obtained by analysing large-scale systems.

KEYWORDS:

bisimulation, boolean equation system, equivalence checking, labelled transition system, modal mu-calculus, model checking, on-the-fly verification, partial order reduction, specification, temporal logic

Back to the VASY Home Page