Distributed On-the-Fly Equivalence Checking

Christophe Joubert and Radu Mateescu

Proceedings of the 3rd Workshop on Parallel and Distributed Methods in Verification PDMC'2004 (London, U.K.), September 2004

Abstract:

On-the-fly equivalence checking consists in comparing two Labeled Transition Systems (LTSs) modulo a given equivalence relation by exploring them in a demand-driven way. Since it avoids the explicit construction of LTSs, this method is able to detect errors even in systems that are too large to fit in the memory of a computer. In this paper, we aim at further improving the performance of on-the-fly equivalence checking using several machines connected by a network. We propose DSOLVE, a new algorithm for distributed on-the-fly resolution of Boolean Equation Systems (BESs), which enables equivalence checking modulo various relations characterized in terms of BESs. DSOLVE serves as verification engine for the distributed version of BISIMULATOR, an on-the-fly equivalence checker developed within the CADP verification toolbox using the OPENCAESAR environment. Our experimental measures show quasi-linear speedups and a good scalability of the distributed version of BISIMULATOR w.r.t. its sequential version.

15 pages

PDF

PostScript

Slides of Ch. Joubert's lecture at PDMC'04

PDF