Distributed Parametric and Statistical Model Checking

TL;DR

This paper demonstrates that Statistical Model Checking can be efficiently parallelized using a master/slaves architecture, significantly improving scalability and performance in verifying complex systems.

Contribution

The paper introduces scalable parallel algorithms for Statistical Model Checking, implemented in UPPAAL SMC, enabling near-linear performance improvements on distributed systems.

Findings

Algorithms scale almost linearly with number of slave computers

Implementation in UPPAAL SMC successfully applied to complex case studies

Parallelization significantly enhances verification efficiency

Abstract

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.