Scaling up statistical model checking of cyber-physical systems via algorithm ensemble and parallel simulations over HPC infrastructures
The paper addresses slow model-based formal verification for complex Cyber-Physical Systems (CPS) by using Statistical Model Checking (SMC). It introduces an Ensemble of Approximation Algorithms (EAA) that combines multiple stopping algorithms to drastically reduce the number of required simulations, achieving up to 78% reduction. Furthermore, it speeds up these simulations significantly by running them in parallel on High-Performance Computing (HPC) infrastructure, making verification feasible in hours or days.