Distributed On-the-Fly Model Checking and Test Case Generation

Christophe Joubert and Radu Mateescu

Proceedings of the 13th International Workshop on Model Checking of Software SPIN'2006 (Vienna, Austria), March-April 2006

Full version available as INRIA Research Report RR-5880.

Abstract:

The explicit-state analysis of concurrent systems must handle large state spaces, which correspond to realistic systems containing many parallel processes and complex data structures. In this report, we combine the on-the-fly approach (incremental construction of the state space) and the distributed approach (state space exploration using several machines connected by a network) in order to increase the computing power of analysis tools. To achieve this, we propose MB-DSOLVE, a new algorithm for distributed on-the-fly resolution of multiple block, alternation-free boolean equation systems (BESs). First, we apply MB-DSOLVE to perform distributed on-the-fly model checking of alternation-free modal mu-calculus, using the standard encoding of the problem as a BES resolution. The speedup and memory consumption obtained on large state spaces improve over previously published approaches based on game graphs. Next, we propose an encoding of the conformance test case generation problem as a BES resolution from which a diagnostic representing the complete test graph is built. By applying MB-DSOLVE, we obtain a distributed on-the-fly test case generator whose capabilities scale up smoothly w.r.t. well-established existing sequential tools.

24 pages

PDF

PostScript

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

PDF