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

PDF

PostScript

Slides of R. Mateescu's lecture at TACAS'05

PDF