Résumé
Toutes les techniques de vérification des cours précédents reposaient sur une représentation implicite des systèmes par des formules Booléennes, symboliques ou numériques. Au contraire, la vérification explicite repose sur une exploration systématique du système à étudier par énumération explicite de ses états et transitions. En pratique, la vérification explicite a des propriétés très différentes de celles des vérifications implicites. Par exemple, elle donne de bons résultats sur les systèmes très asynchrones comme les protocoles de communication et les algorithmes distribués, souvent moins bien adaptés à la vérification implicite qui est elle très performante pour les systèmes synchrones. D’autre part, elle se parallélise bien, ce qui n’est pas encore le cas pour les algorithmes implicites.
Mais, pour que la vérification explicite soit efficace, il faut impérativement implémenter certaines optimisations délicates : systèmes de caches efficaces et de très grande taille pour la détection des états déjà visités, réductions d’ordres partiels pour éviter d’énumérer dans tous les ordres possibles des suites d’actions indépendantes, interprétation abstraite par hashcodes ne traitant pas les collisions, utilisation systématique de l’aléatoire, etc.
Le cours présente les algorithmes explicites et leurs applications à travers deux des principaux systèmes du domaine : SPIN, développé par G. Holtzmann aux Bell Labs, et CADP, développé à l’Inria par H. Garavel, R. Mateescu et leur équipe. SPIN est un système compact fondé sur un langage de spécification issu de C, simple d’usage, mais relativement limité, alors que CADP de présente sous la forme d’une grande librairie d’algorithmes combinables entre eux et gérés par un langage de script. CADP prend comme entrée des spécifications écrites dans divers calculs algébriques de processus communicants, et résout des problèmes d’énumération, d’équivalence par bisimulation, de preuves hiérarchiques par réductions compositionnelles, etc. SPIN et CADP ont tous deux des groupes d’utilisateurs académiques et industriels très actifs.
