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.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00011939 |
| Date | 12 December 2005 |
| Creators | Joubert, Christophe |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0017 seconds