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
Reports

Parallel State Space Construction for Model-Checking

Hubert Garavel 1 Radu Mateescu 1 Irina Smarandache 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The verification of concurrent finite-state systems by model-checking often requires to generate (a large part of) the state space of the system under analysis. Because of the state explosion problem, this may be a resource-consuming operation, both in terms of memory and CPU time. In this report, we aim at improving the performances of state space construction by using parallelization techniques. We present parallel algorithms for constructing state spaces (or Labeled Transition Systems) on a network or a cluster of workstations. Each node in the network builds a part of the state space, all parts being merged to form the whole state space upon termination of the parallel computation. These algorithms have been implemented within the CADP verification tool set and experimented on various concurrent applications specified in LOTOS. The results obtained show linear speedups and a good load balancing between network nodes.
Document type :
Reports
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072247
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 8:13:10 PM
Last modification on : Friday, February 4, 2022 - 3:21:50 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:39:40 PM

Identifiers

  • HAL Id : inria-00072247, version 1

Collections

Citation

Hubert Garavel, Radu Mateescu, Irina Smarandache. Parallel State Space Construction for Model-Checking. [Research Report] RR-4341, INRIA. 2001. ⟨inria-00072247⟩

Share

Metrics

Record views

2606

Files downloads

22276