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

Highlights

• Model-based verification of industry-relevant CPSs is often computationally prohibitive.Source: Highlights · p. 2
• The Ensemble of Approximation Algorithms (EAA) combines multiple stopping algorithms (SAs) to minimize the number of required system simulations.The implementation is ∼100% efficient even on large HPC infrastructures.Source: Highlights · p. 2
• Complex CPS verification tasks can take hours or days with the combined approach, compared with months to many years for naïve sequential execution.Source: Highlights · p. 2

1. Introduction

• CPS state spaces grow exponentially with the number of modeled variables, making exhaustive model checking impractical within realistic time frames.SMC instead produces KPI approximations with user-defined probabilistic guarantees, though it cannot generally provide definite answers.Source: §1 · p. 3

1.1. Motivation

• The sample count needed by an adaptive stopping algorithm depends on unknown KPI statistics, and excess samples are costly because each requires numerical system simulation.The paper motivates running an ensemble because different stopping algorithms may need different sample counts for a given problem.Source: §1.1 · p. 4

1.2. Contribution

• EAA concurrently runs multiple stopping algorithms on the same iid samples and stops when the first algorithm converges with the requested guarantees.The evaluation combines EBGStop and AA on three industrial-size Simulink/Stateflow CPS models.Source: §1.2 · p. 4
• Up to 31 300 400 and up to 78.73% fewer samples are required than when running a single adaptive stopping algorithm.The authors also report efficiency very close to 100% for parallel sample generation, even on large platforms.Source: §1.2 · p. 4

1.3. Outline

• The article proceeds from preliminaries and the formal framework to EAA, its parallel implementation, experiments, and conclusions.Source: §1.3 · p. 5

2. Preliminaries and related work

• The section introduces notation and two optimal stopping algorithms, AA and EBGStop, whose sample requirements can differ with the problem.AA is fully optimal for bounded non-negative random variables, while EBGStop's optimality expression also depends on the variable's range.Source: §2 · p. 5, §2.2 · p. 6

2.1. Unbiased estimators

• An (ε, δ)-estimator has a sample size that yields an estimate within relative error ε of the parameter with probability greater than 1 − δ.For an expected value, the sample mean is unbiased under distribution-matched sampling and is an (ε, δ)-estimator by the central limit theorem.Source: §2.1 · p. 5

2.2. Adaptive Stopping Algorithms

• Classical Monte Carlo methods fix sample size in advance and may overshoot, ignore the random variable's properties, and fail to update their estimate during execution.Source: §2.2 · p. 5
• An adaptive stopping algorithm updates its estimate and stopping criterion as samples arrive, stopping when the sample count guarantees an (ε, δ)-approximation.Such algorithms use accumulated sample information to decide when the requested statistical guarantees are met.Source: §2.2 · p. 5
• Stopping criteria must be justified by their underlying statistical results; the NAS algorithm uses a Hoeffding-derived criterion, while EBStop uses the empirical Bernstein inequality.EBGStop further uses geometric sampling, accumulating samples at an exponential rate β.Source: §2.2 · pp. 5–6

• CPS verification checks system requirements using a system model, operational scenarios, and a formalized specification.Source: §3 · pp. 6–7
• The SUV is modeled as a deterministic input-output system that maps an operational scenario to an output trajectory.Source: §3 · p. 7
• The environment pairs possible scenarios with probabilities and is restricted to finitely parameterizable scenarios represented by finite-dimensional vectors.Source: §3 · p. 7
• Verification assesses whether the expected value of a normalized KPI is at most a threshold, using an approximation with precision ε and confidence level 1−δ.Source: §3 · pp. 7–8

• A single stopping algorithm may generate unnecessary samples because convergence depends on unknown KPI statistics, even for algorithms with probabilistic sample-count optimality.Source: §4 · p. 8
• Each generated KPI sample advances every algorithm in the ensemble by one step.For CPS verification, a sample is generated by simulating the model under a random scenario and computing its KPI.Source: §4 · p. 8
• EAA returns the first algorithm’s estimate to meet its termination condition, which is a valid (ε, δ)-approximation of the KPI mean.Source: §4 · p. 8
• EAA needs the minimum number of samples that any member would require if run alone, because it stops when the first algorithm meets its stopping criterion.Source: §4 · p. 8
• Each ensemble member can be advanced by refactoring an approximation algorithm to process one sample and update its persistent state; this adds few algebraic operations.The simulation time per sample is expected to be much longer than the cost of advancing the algorithms.Source: §4 · p. 8

• SMC case studies required over 100 million samples, and single-sample simulation times ranged from 0.1 seconds to several seconds.Source: §5 · p. 10
• HPC-EAA uses n identical simulators and an asynchronous sample generator to delegate scenario simulations while ensemble algorithms process samples concurrently.Source: §5 · p. 10
• APSG generates scenarios, assigns them to idle simulators, stores completed KPI values by scenario ID, and returns them to the algorithms in order.The bounded sample map blocks insertion when full and consumption waits until the next ordered sample is available.Source: §5 · p. 10
• For the same random seed, APSG supplies the same scenario sequence as the sequential sampler, so increasing simulator count raises sample availability without changing sample order.The authors state that this avoids bias in sample pseudorandomness and the resulting approximation.Source: §5 · p. 10

• The experiments use three industrial case-study models to perform model-based SMC verification tasks.Source: §6 · p. 12
• The combined ensemble and massively parallel simulations complete verification tasks within a reasonable time frame, unlike a naïve implementation.Source: §6 · p. 12
• A naïve implementation would have taken an inconceivably long time for the reported verification tasks.Source: §6 · p. 12

6.1. Case studies

• The three industry-scale case studies are Automatic Transmission (AT), Fuel Control System (FCS), and Apollo Lunar Module Autopilot (ALMA).All three are Simulink/Stateflow models.Source: §6.1 · p. 12

6.1.1. Automatic Transmission (AT)

• The verification assesses whether expected maximum time violation over h=1,800 s is at most 5%, using speed and engine-speed thresholds of 4,000 RPM and 120 RPM.The brake is set to zero, and throttle varies around an average of 40% with variance 20.Source: §6.1.1 · p. 12

6.1.2. Fuel Control System (FCS)

• FCS checks whether the expected longest interval of zero fuel flow exceeds 1% of the 105 s evaluation horizon, excluding the first 5 s.Temporary faults are injected on the engine-speed, exhaust-oxygen, and manifold-pressure sensors, with recovery durations drawn from an exponential distribution.Source: §6.1.2 · p. 13

6.1.3. Apollo Lunar Module Autopilot (ALMA)

• ALMA evaluates expected normalized mean attitude error against a 0.5% threshold over a 60 s mission, with temporary faults modeled as sensor noise.The KPI aggregates attitude errors across yaw, pitch, and roll, normalized by 2π.Source: §6.1.3 · pp. 13–14

6.2. Implementation

• The production software is implemented in Python and Cython and uses MPI for interprocess communication.MPI is the Message Passing Interface standard.Source: §6.2 · p. 14
• HPC-EAA runs the SAs and APSG as concurrent threads, while simulators run as independent processes on additional computational nodes.The architecture is designed for networked HPC infrastructures.Source: §6.2 · p. 14
• Separate HPC-EAA threads advance each SA, generate and dispatch random scenarios, and process returned samples into the samples map.This thread-based arrangement limits network communication to exchanges with simulators.Source: §6.2 · p. 14

6.3. Experimental setting

• The study evaluated 9 ε values, 3 δ values, and 7 simulator counts from 1 to 2,048, repeating each experiment 10 times with independent iid-scenario sequences.Each case study used 10 random experiments for each setting.Source: §6.3 · pp. 14–15
• 10 repeated runs per case study across ε, δ, and n settings would require decades of production-tool execution and up to 2,052 computational nodes per run.The study therefore used an indirect performance-analysis approach.Source: §6.3 · p. 14
• The team precomputed 10 scenario sequences per case study, then measured each scenario’s simulation time and KPI value in separate HPC jobs.Average simulation times were 0.1377 s for AT, 0.2279 s for FCS, and 7.1654 s for ALMA.Source: §6.3 · p. 15
• A discrete-event emulator replayed instrumented tool steps with precomputed samples to estimate execution faster than real time.The emulator accumulated measured and database-sourced step durations while orchestrating the experiment.Source: §6.3 · p. 15
• The estimates may diverge slightly from actual production runs because code disassembly and instrumentation can introduce small differences.The authors characterize the estimates as what would occur on bare metal, while HPC orchestration and virtualization can add noise.Source: §6.3 · p. 15
• Figure 3 plots EAA convergence sample counts on a log-scale axis and the savings against the algorithm requiring the most samples, across 10 experiments and ε, δ settings.The figure caption describes the comparison but does not provide cell values.Source: Figure 3 · p. 16

6.4.1. Reduction of the number of required samples due to EAA

• EAA required up to 31 300 400 fewer samples than a single algorithm, with relative reductions as large as 78.73%.The saving is measured against using only the slower of the two SAs.Source: §6.4.1 · p. 16
• For a fixed case study and δ, EAA's required-sample curves nearly overlapped across different random sample sequences.Which SA finishes first is difficult to predict because it depends on ε, δ, KPI statistics, and the sample sequence.Source: §6.4.1 · p. 16

6.4.2. Increase of the sample production rate due to the Asynchronous Parallel Sample Generator

• Across simulator counts, APSG sample production rates were practically linear in n, with maximum deviation from ideal linear rates below 0.1%.The rates were measured by requesting and discarding one million samples at each n.Source: §6.4.2 · p. 17
• EAA's sample-consumption rate exceeded APSG production rates by several orders of magnitude, remaining more than 100 times higher at n = 2048.The authors infer that the SAs module would spend almost all its time waiting for APSG to produce samples.Source: §6.4.2 · p. 17

6.4.3. Overall performance scalability analysis

• Completion-time curves were qualitatively similar across cases, with reductions essentially proportional to n.Figure 5 reports average completion times and minimum-to-maximum error bars across 10 experiments.Source: §6.4.3 · pp. 17–18
• Estimated parallel efficiency stayed near 100%, except when excessive simulator counts generated samples that EAA never used.The authors characterize that exception as hardware over-dimensioning; completion time was then only a few seconds or minutes.Source: §6.4.3 · p. 18

7. Conclusions and perspectives

• EAA combines the respective strengths of multiple stopping algorithms; the tested implementation paired EBGStop and AA with a massively parallel HPC architecture.Source: §7 · p. 18
• Across three industry-scale case studies, the authors report that parallelization can make SMC viable for verifying complex systems despite prohibitive sequential simulation counts.They argue parallelization should be considered systematically to widen SMC applicability.Source: §7 · p. 18
• Future directions include adding other stopping algorithms, supporting formula-based properties and hyper-properties, and exploring parallelizable SMC optimization algorithms and improved sampling.The text specifically mentions geometric sampling as a possible improvement.Source: §7 · p. 18