Joubert-05

Vérification distribuée à la volée de grands espaces d´états

Christophe Joubert

Thèse de doctorat en informatique de l'Institut National Polytechnique de Grenoble (Montbonnot, France), December 2005

RESUME :

La vérification des systèmes d'états finis, qu'ils soient distribués ou concurrents, est confrontée en pratique au problème d'explosion d'états (taille prohibitive de l'espace d'états sous-jacent) qui survient pour des systèmes de taille réaliste, contenant de nombreux processus en parallèle et des structures de données complexes. Différentes techniques ont été proposées pour combattre l'explosion d'états, telles que la vérification à la volée, la réduction d'ordre partiel, ou encore la vérification distribuée. Cependant, l'expérience pratique a montré qu'aucune de ces techniques, à elle seule, n'est toujours suffisante pour maîtriser des systèmes à grande échelle.

Cette thèse propose une combinaison de ces approches dans le but de faire passer à l'échelle leurs capacités de vérification. Notre approche est basée sur les Systèmes d'Equations Booléennes (SEBs), qui fournissent une représentation intermédiaire élégante des problèmes de vérification définis sur des Systèmes de Transitions Etiquetées, comme la comparaison par équivalence, la réduction par tau-confluence, l'évaluation de formules de mu-calcul modal sans alternance, ou encore la génération de cas de tests de conformité.

Nous proposons DSolve et MB-DSolve, deux nouveaux algorithmes pour la résolution distribuée à la volée de SEBs (contenant un, resp. plusieurs blocs d'équations), et nous les employons comme moteurs de calcul pour quatre outils de vérification à la volée développés au sein de la boîte à outils CADP en utilisant l'environnement OPEN/CAESAR : le comparateur par équivalence BISIMULATOR, le réducteur TAU_CONFLUENCE, l'évaluateur de propriétés temporelles EVALUATOR, et le générateur de cas de tests de conformité EXTRACTOR. Les mesures expérimentales effectuées sur des grappes de machines montrent des accélérations quasi-linéaires et un bon passage à l'échelle des versions distribuées de ces outils par rapport à leurs équivalents séquentiels.

MOTS-CLES :

système d'équations booléennes, algorithme à mémoire distribuée, vérification à la volée, comparaison par équivalence, réduction d'ordre partiel, évaluation de formules de logique temporelle, génération de cas de tests de conformité

TITLE:

Distributed On-the-Fly Verification of Large State Spaces

ABSTRACT:

The verification of concurrent finite-state systems is confronted in practice with the state explosion problem (prohibitive size of the underlying state space), which occurs for realistic systems containing many parallel processes and complex data structures. Various techniques for fighting against state explosion have been proposed, such as on-the-fly verification, partial order reduction, and distributed verification. However, practical experience has shown that none of these techniques alone is always sufficient to handle large-scale systems.

In this thesis, we propose a combination of these approaches in order to scale up their capabilities. Our approach is based upon Boolean Equation Systems (BESs), which provide an elegant intermediate representation for verification problems defined on Labeled Transition Systems, such as equivalence checking, tau-confluence reduction, model checking of alternation-free mu-calculus, and test-case generation.

We propose DSolve and MB-DSolve, two new algorithms for distributed on-the-fly resolution of BESs (containing one, resp. several equation blocks), and employ them as computing engines for four on-the-fly verification tools developed within the CADP toolbox using the OPEN/CAESAR environment: the BISIMULATOR equivalence checker, the TAU_CONFLUENCE reductor, the EVALUATOR model checker, and the EXTRACTOR test-case generator. Experimental measures performed on clusters of machines show quasi-linear speedups and a good scalability of the distributed versions of these tools w.r.t. their sequential counterparts.

KEYWORDS:

boolean equation system, distributed memory algorithm, on-the-fly verification, equivalence checking, partial order reduction, model checking, test case generation

172 pages (in French)
PDF
PostScript


Slides of Ch. Joubert's thesis defense (in French)
PDF



Slides of Ch. Joubert's thesis defense (in English)
PDF