Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems

Radu Mateescu 1 Emilie Oudot 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Equivalence checking is a classical verification method determining if a finite-state concurrent system (protocol) satisfies its desired external behaviour (service) by comparing their underlying labeled transition systems (LTSs) modulo an appropriate equivalence relation. Local (or on-the-fly) equivalence checking explores the synchronous product of the LTSs incrementally, allowing an efficient detection of errors in complex systems. In this paper, we consider the technique based on translating the equivalence checking problem in terms of the local resolution of a boolean equation system (BES). We propose two enhancements of this technique in the case of equivalent LTSs: a new, faster BES encoding of weak equivalence relations, and a new local BES resolution algorithm with a good average complexity. These enhancements were incorporated into the BISIMULATOR 2.0 equivalence checker of the CADP toolbox, and led to significant performance improvements.
Type de document :
Communication dans un congrès
Stephen A. Edwards and Klaus Schneider. MEMOCODE'2008, Jun 2008, Anaheim, United States. IEEE Computer Society Press, 2008, 〈10.1109/MEMCOD.2008.4547690〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00357770
Contributeur : Radu Mateescu <>
Soumis le : dimanche 1 février 2009 - 23:07:26
Dernière modification le : mercredi 11 avril 2018 - 01:51:56
Document(s) archivé(s) le : vendredi 12 octobre 2012 - 10:31:27

Fichier

Mateescu-Oudot-08-a.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Radu Mateescu, Emilie Oudot. Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems. Stephen A. Edwards and Klaus Schneider. MEMOCODE'2008, Jun 2008, Anaheim, United States. IEEE Computer Society Press, 2008, 〈10.1109/MEMCOD.2008.4547690〉. 〈inria-00357770〉

Partager

Métriques

Consultations de la notice

354

Téléchargements de fichiers

114