dmcG: a distributed symbolic model checker based on GreatSPN

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.
Type de document :
Communication dans un congrès
28th International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2007), Jun 2007, Siedlce, Poland. Springer, ICATPN'07 Proceedings of the 28th international conference on Applications and theory of Petri nets and other models of concurrency, 4546, pp.495-504, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-73094-1_29〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00701513
Contributeur : Ist Rennes <>
Soumis le : vendredi 25 mai 2012 - 15:17:17
Dernière modification le : vendredi 31 août 2018 - 09:25:57

Identifiants

Collections

Citation

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. Springer, ICATPN'07 Proceedings of the 28th international conference on Applications and theory of Petri nets and other models of concurrency, 4546, pp.495-504, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-73094-1_29〉. 〈hal-00701513〉

Partager

Métriques

Consultations de la notice

106