HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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

Christophe Joubert 1 Radu Mateescu 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Document type :
Complete list of metadata

Cited literature [38 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 5:07:33 PM
Last modification on : Friday, February 4, 2022 - 3:22:47 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:09:22 PM


  • HAL Id : inria-00071388, version 1



Christophe Joubert, Radu Mateescu. Distributed On-the-Fly Model Checking and Test Case Generation. [Research Report] RR-5880, INRIA. 2006. ⟨inria-00071388⟩



Record views


Files downloads