Optimizing Highly-Parallel Simulation-Based Verification of Cyber-Physical Systems

Cyber-Physical Systems (CPSs), comprising both software and physical components, arise in many industry-relevant domains and are often mission- or safety-critical. System-Level Verification (SLV) of CPSs aims at certifying that given (e.g., safety or liveness) specifications are met, or at estimating the value of some Key Performance Indicators, when the system runs in its operational environment, that is in presence of inputs and/or of additional, uncontrolled disturbances. To enable SLV of complex systems from the early design phases, the currently most adopted approach envisions the simulation of a system model under the (time bounded) operational scenarios deemed of interest. Unfortunately, simulation-based SLV can be computationally prohibitive (years of sequential simulation), since system model simulation is computationally intensive and the set of scenarios of interest can be extremely large. In this article, we present a technique that, given a collection of scenarios of interest (extracted from databases or from symbolic structures), computes parallel shortest simulation campaigns, which drive a possibly large number of system model simulators running in parallel in a HPC infrastructure through all (and only) those scenarios in the user-defined (possibly random) order, by wisely avoiding multiple simulations of repeated trajectories, thus minimising completion time. Our experiments on SLV of Modelica/FMU and Simulink models with up to almost 200 million scenarios show that our optimisation yields speedups as high as 8 x. This, together with the enabled massive parallelisation, makes practically viable (a few weeks in a HPC infrastructure) verification tasks (both statistical and exhaustive) which would otherwise take inconceivably long time.