PostScript
BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking
Damien Bergamini, Nicolas Descoubes, Christophe Joubert, and Radu Mateescu
Proceedings of the 11th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
TACAS'2005 (Edinburgh, Scotland), April 2005
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. Global verification requires to construct the two LTSs before comparison, whereas local (or on-the-fly) verification allows to explore them incrementally during comparison, thus being more suitable for detecting errors in large systems. In this paper, we present BISIMULATOR, an efficient on-the-fly equivalence checker with a highly modular architecture, developed within the CADP verification toolbox. The front-end of the tool encodes five widely-used equivalence relations in terms of Boolean Equation Systems (BESs) by using the OPEN/CAESAR and BCG environments of CADP, which provide powerful LTS exploration primitives. The back-end carries out the verification by using the generic CAESAR_SOLVE library of CADP, dedicated to (sequential and distributed) on-the-fly BES resolution and diagnostic generation. The sequential version of BISIMULATOR compares favourably with other specialized on-the-fly equivalence checking tools, and the distributed version exhibits linear speedups w.r.t. the sequential one.
| 5 pages | |
PostScript |
| Slides of R. Mateescu's lecture at TACAS'05 | |