Distributed Parametric and Statistical Model Checking

Peter Bulychev
(Aalborg University)
Alexandre David
(Aalborg University)
Kim Guldstrand Larsen
(Aalborg University)
Marius Mikučionis
(Aalborg University)
Axel Legay
(Aalborg University and INRIA Rennes)

Statistical Model Checking (SMC) is a trade-off between testing and formal verification. The core idea of the approach is to conduct some simulations of the system and verify if they satisfy some given property. In this paper we show that SMC is easily parallelizable on a master/slaves architecture by introducing a series of algorithms that scale almost linearly with respect to the number of slave computers. Our approach has been implemented in the UPPAAL SMC toolset and applied on non-trivial case studies.

Invited Presentation in Jiří Barnat and Keijo Heljanko: Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2011), Snowbird, Utah, USA, July 14, 2011, Electronic Proceedings in Theoretical Computer Science 72, pp. 30–42.
Published: 31st October 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.72.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org