Skip to Main content Skip to Navigation
Conference papers

dmcG: a distributed symbolic model checker based on GreatSPN

Alexandre Hamez 1 Fabrice Kordon 1 yann Thierry-Mieg 1 Fabrice Legond-Aubry 1 
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : We encountered some limits when using the GreatSPN model checker on life-size models, both in time and space complexity. Even when the exponential blow-up of state space size is adequately handled by the tool thanks to the use of a canonization function that allows to exploit system symmetries, time complexity becomes critical. Indeed the canonization procedure is computationally expensive, and verification time for a single property may exceed 2 days (without exhausting memory). Using the GreatSPN model-checking core, we have built a distributed model-checker, dmcG, to benefit from the aggregated resources of a cluster. We built this distributed version using a flexible software architecture dedicated to parallel and distributed model-checking, thus allowing full reuse of GreatSPN source code at a low development cost. We report performances on several specifications that show we reach the theoretical linear speedup w.r.t. the number of nodes. Furthermore, through intensive use of multi-threading, performances on multiprocessors architectures reach a speedup linear to the number of processors.
Document type :
Conference papers
Complete list of metadata
Contributor : Ist Rennes Connect in order to contact the contributor
Submitted on : Friday, May 25, 2012 - 3:17:17 PM
Last modification on : Sunday, June 26, 2022 - 9:38:26 AM

Links full text



Alexandre Hamez, Fabrice Kordon, yann Thierry-Mieg, Fabrice Legond-Aubry. dmcG: a distributed symbolic model checker based on GreatSPN. 28th International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2007), Jun 2007, Siedlce, Poland. pp.495-504, ⟨10.1007/978-3-540-73094-1_29⟩. ⟨hal-00701513⟩



Record views