DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation

Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, and Gilles Stragier

Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2006 (Vienna, Austria), April 2006

Abstract:

The verification of complex finite-state systems, whose underlying state spaces may be prohibitively large, requires an important amount of memory and computation time. A natural way of scaling up the capabilities of verification tools is by exploiting the computing resources (memory and processors) of massively parallel machines, such as clusters and grids. This paper describes DISTRIBUTOR, a tool for generating state spaces in a distributed manner using a set of machines connected by a network. Each machine is responsible for generating and storing a part of the state space. Upon termination of the distributed generation, all parts generated by the machines are combined together using the BCG_MERGE tool in order to obtain the complete state space. DISTRIBUTOR was developed within the CADP verification toolbox using the generic OPEN/CAESAR environment for on-the-fly graph exploration. It exhibits good speedups compared to sequential tools, implements on-the-fly reductions of the state space, and provides graphical features for monitoring the distributed state space generation in real time.

5 pages

PDF

PostScript

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

PDF