|
 
|
[PP06a] Distributed colored Petri net model-checking with Cyclades
Conférence Internationale avec comité de lecture : PDMC'06 Proceedings Parallel and Distributed Methods in verifiCation, January 2006, pp.347-361, Series LNCS, (DOI: 10.1007/978-3-540-70952-7_24)
motcle:
Résumé:
The major bottleneck of explicit model-checking tools is the limited amount of available memory.Distributed model-checking is an approach to tackle the combinatorial explosion problem. It consists in taking advantage of the aggregate of memory provided by a network of workstations to increase the amount of memory available for model-checking.
Helena is the model-checker of the Quasar tool suite for concurrent software verification. It is a high-level colored Petri net explicit sequential model-checker that implements several state-space reduction and efficient state representation mechanisms. Helena is currently able to verify safety properties. In this paper we present Cyclades, a distributed version of Helena, that remains compatible with these reduction techniques. Several distribution mechanisms and some preliminary results are also provided.
BibTeX
| @inproceedings { | |||
| PP06a, | |||
| title | = | "{Distributed colored Petri net model-checking with Cyclades}", | |
| author | = | " C. Pajault and J. Pradat-Peyre ", | |
| booktitle | = | "{PDMC'06 Proceedings Parallel and Distributed Methods in verifiCation}", | |
| year | = | 2006, | |
| month | = | "January", | |
| series | = | "LNCS", | |
| pages | = | "347-361", | |
| doi | = | "10.1007/978-3-540-70952-7_24", | |
| } | |||
