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

The gist The number of model simulations required by Statistical Model Checking (SMC) techniques can be significantly reduced by considering multiple Adaptive Stopping Algorithms (SAs) at once, and that the simulations themselves can be efficiently sped up by exploiting massively parallel platforms.

How it works

The paper addresses the computational prohibitive nature of model-based formal verification for Cyber-Physical Systems (CPSs), where exhaustive simulation is rarely possible, necessitating Statistical Model Checking (SMC) [3]. The core contribution is the Ensemble of Approximation Algorithms (EAA), a composite algorithm that concurrently runs a set of different SAs by feeding them iid samples and terminating as soon as the first SA converges [1.2]. This ensemble approach aims to minimize the number of required system simulations by combining multiple SAs, such as EBGStop and AA, which can lead to reductions in sample size of up to 78% compared to running a single algorithm [6.4.1].

Ensemble of Approximation Algorithms (EAA)

The EAA algorithm is designed as a general procedure that exploits a finite set A1,..., Ak of different (ε, δ)-approximation algorithms [4]. The procedure initializes the states of all algorithms in the ensemble and then repeatedly generates samples of random variable X, simulating the SUV model on each sample to compute the associated KPI value [2.2]. Each sample x is then used to feed and advance all algorithms in the ensemble by one step only, terminating as soon as one algorithm reaches its stopping condition [4]. This design ensures that the number of samples required by EAA is always the minimum number of samples that would have been required by each algorithm in the ensemble if it were run alone [4].

Massively Parallel Simulation over HPC Infrastructures

A second major bottleneck addressed is the rate at which samples are provided to the approximation algorithm, as generating a single sample can take significant time [5]. The solution involves exploiting High-Performance Computing (HPC) infrastructures by using many identical simulators running in parallel on n additional computational nodes [10]. The architecture implements a producer-consumer paradigm where an Asynchronous Parallel Sample Generator (APSG) continuously generates random scenarios and delegates the simulation of each scenario to one of the n available parallel simulators [10]. This setup ensures that the order of the scenarios generated is independent of the number n of simulators [10], thereby avoiding bias in the final result [10].

Experimental Results and Scalability

The study was conducted on three industry-scale CPS models: Automatic Transmission (AT) [6.1.1], Fuel Control System (FCS) [6.1.2], and Apollo Lunar Module Autopilot (ALMA) [6.1.3]. The results demonstrate that the combined effect of EAA and massively parallelization allows verification tasks to be completed in a matter of hours or days, whereas a naïve sequential execution would require from months to many years [Abstract]. Specifically, EAA can reduce the number of necessary samples by up to 31 300 400 when compared to using a single algorithm [6.4.1]. Furthermore, the efficiency of the parallelization shows that the estimated efficiency always sticks to ∼ 100%, except when the number of simulators (hence, the size of the envisioned HPC infrastructure) is too large for the problem at hand [6.4.3].

Conclusion and Perspectives

The work confirms that parallelization should be considered as systematically as possible to increase and widen the applicability of SMC [7]. The authors successfully implemented EAA using EBGStop and AA, showing that this approach makes SMC a viable method for verifying complex systems even when simulation costs are prohibitive [7]. Future work could involve extending EAA to integrate other SAs or exploring verification of formula-based properties such as linear temporal logic [7].

--- Page 1 ---

The gist The number of model simulations required by Statistical Model Checking (SMC) techniques can be significantly reduced by considering multiple Adaptive Stopping Algorithms (SAs) at once, and that the simulations themselves can be efficiently sped up by exploiting massively parallel platforms.

Massively Parallel Simulation over HPC Infrastructures

A second major bottleneck addressed is the rate at which samples are provided to the approximation algorithm, as generating a single sample can take significant time [5]. The solution involves exploiting High-Performance Computing (HPC) infrastructures by using many identical simulators running in parallel on n additional computational nodes [10].

1. Bold Ensemble of Approximation Algorithms (EAA) for Sample Reduction: The EAA algorithm is proposed as a composite algorithm that concurrently runs a set (ensemble) of different SAs to minimize the number of required system simulations. This allows the improved AI system to achieve reductions in sample size of up to 78% compared to running a single SA, significantly lowering the computational cost for model-based Statistical Model Checking (SMC) verification.

2. Bold Massively Parallel Simulation Execution: The implementation exploits HPC infrastructure by massively parallelizing system model simulations on a HPC infrastructure, achieving an efficiency of virtually 100% even on large platforms. This enables the AI system to complete complex CPS verification tasks in a matter of hours or days, whereas a naïve sequential execution would require from months to many years.

3. Bold Scalable Performance Analysis: The tool provides a performance scalability analysis where the estimated efficiency always sticks to ∼ 100% when using parallel simulators, suggesting that adding more algorithms to the ensemble of SAs would not introduce any noticeable computational overhead. This allows for predictable and efficient scaling of verification tasks as the required number of parallel nodes increases.

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.