Scaling up statistical model checking of cyber-physical systems via algorithm ensemble and parallel simulations over HPC infrastructures

• Published in: The Journal of systems and software 2025-01, Vol.219, p.112238, Article 112238
• Main Authors: Picchiami, Leonardo, Parmentier, Maxime, Legay, Axel, Mancini, Toni, Tronci, Enrico
• Format: Article
• Language: English
• Subjects: Adaptive Stopping Algorithms; Cyber-Physical Systems; Formal verification; High-Performance Computing; Monte Carlo estimation; Simulation; Statistical Model Checking
• ISSN: 0164-1212
• DOI: 10.1016/j.jss.2024.112238

Model-based formal verification of industry-relevant Cyber-Physical Systems (CPSs) is often a computationally prohibitive task. In most cases, the complexity of the models precludes any prospect of symbolic analysis, leaving numerical simulation as the only viable option. Unfortunately, exhaustive simulation of a CPS model over the entire set of plausible operational scenarios is rarely possible in practice, and alternative strategies such as Statistical Model Checking (SMC) must be used instead. In this article, we show that the number of model simulations (samples) required by SMC techniques to converge can be significantly reduced by considering multiple (an ensemble of) Adaptive Stopping Algorithms (SAs) at once, and that the simulations themselves (by far the most expensive step of the entire workload) can be efficiently sped up by exploiting massively parallel platforms. With three industry-scale CPS models, we experimentally show that the use of an ensemble of two state-of-the-art SAs (AA and EBGStop) may require dozens of millions fewer samples when compared to running a single algorithm, with reductions in sample size of up to 78%. Furthermore, we show that our implementation, by massively parallelizing system model simulations on a HPC infrastructure, yields speed-ups for the completion time of the verification tasks which are practically linear with respect to the number of computational nodes, thus achieving an efficiency of virtually 100%, even on very large platforms. This makes it possible to complete tasks of model-based SMC verification for complex CPSs in a matter of hours or days, whereas a naïve sequential execution would require from months to many years. •Model-based verification of industry-relevant Cyber-Physical Systems (CPSs) is often computationally prohibitive.•Simulation-based Statistical Model Checking (SMC) approaches in the form of Adaptive Stopping Algorithms (SAs) are often necessary to handle complex models.•Our Ensemble of Approximation Algorithms (EAA) combines multiple SAs to minimize the number of required system simulations.•Our implementation massively parallelizes model simulations on HPC platforms, and is ∼100% efficient even on large infrastructures.•As a combined effect of the above, model-based SMC verification tasks of complex CPSs are shown to be completed in hours or a few days, whereas a naïve sequential execution would require from months to many years.