Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [38 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071388
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 5:07:33 PM
Last modification on : Thursday, November 19, 2020 - 1:00:27 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:09:22 PM

Identifiers

  • HAL Id : inria-00071388, version 1

Collections

Citation

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

Share

Metrics

Record views

235

Files downloads

560