BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking

Damien Bergamini Nicolas Descoubes Christophe Joubert Radu Mateescu 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The equivalence checking problem consists in verifying that a system (e.g., a protocol) matches its abstract specification (e.g., a service) by comparing their Labeled Transition Systems (Ltss) modulo a given equivalence relation. Two approaches are traditionally used to perform equivalence checking: global verification requires to construct the two Ltss before comparison, whereas local (or on-the-fly) verification allows to explore them incrementally during comparison. The latter approach is able to detect errors even in prohibitively large systems, and therefore reveals more effective in combating state explosion.
Type de document :
Communication dans un congrès
Nicolas Halbwachs and Leonore D. Zuck. TACAS 2005, Apr 2005, Edinburgh, United Kingdom. Springer, 3440, pp.581-585, 2005, Lecture Notes in Computer Science. 〈10.1007/978-3-540-31980-1_42〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00685325
Contributeur : Ist Rennes <>
Soumis le : mercredi 4 avril 2012 - 17:08:27
Dernière modification le : mercredi 11 avril 2018 - 01:54:32

Identifiants

Collections

Citation

Damien Bergamini, Nicolas Descoubes, Christophe Joubert, Radu Mateescu. BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. Nicolas Halbwachs and Leonore D. Zuck. TACAS 2005, Apr 2005, Edinburgh, United Kingdom. Springer, 3440, pp.581-585, 2005, Lecture Notes in Computer Science. 〈10.1007/978-3-540-31980-1_42〉. 〈hal-00685325〉

Partager

Métriques

Consultations de la notice

259