Abstract FR:

On etudie la mise en Œuvre d'outils de verification automatique dans le cadre des processus paralleles et communiquants representes par des systemes de transitions. Le principe de verification repose sur des notions d'equivalences comportementales entre ces systemes de transitions, rassembles sous le terme de bisimulation. On s'interesse a la minimisation de ces systemes par ces equivalences et l'on presente dans un premier temps quelques ameliorations de l'algorithmique classique du calcul de ces equivalences que l'on met en Œuvre a travers un outil appele fctool. Dans un deuxieme temps, on s'interesse aux reseaux de processus et l'on concentre notre travail sur le probleme de l'explosion combinatoire que l'on rencontre lors du calcul d'un systeme de transitions global lie a un reseau: on contourne le probleme en introduisant une algorithmique originale basee sur la representation implicite des entites composant un systeme de transitions. On utilise une structure de donnees permettant ce type de representation et surtout, une algorithmique efficace pour la manipulation symbolique de ces systemes: celle-ci est connue sous le nom de bdd (pour binary decision diagramm). On etudie la mise en Œuvre de ces techniques par l'implementation d'un outil que l'on appelle hoggar