Optimising Highly-Parallel Simulation-Based Verification of Cyber-Physical Systems
Toni Mancini, Igor Melatti, Enrico Tronci. IEEE Transactions on Software Engineering, 49(9), pages 4443-4455, 2023.
Toni Mancini, Igor Melatti, Enrico Tronci.
Optimising Highly-Parallel Simulation-Based Verification of Cyber-Physical Systems.
IEEE Transactions on Software Engineering, 49(9), pages 4443-4455, 2023.
DOI: 10.1109/TSE.2023.3298432BibTex entry
@ARTICLE{mancini-etal:2023:tse, TITLE = {Optimising Highly-Parallel Simulation-Based Verification of Cyber-Physical Systems}, AUTHOR = {Mancini, T. and Melatti, I. and Tronci, E.}, DOI = {10.1109/TSE.2023.3298432}, ISSN = {0098-5589}, JOURNAL = {{IEEE} Transactions on Software Engineering}, PUBLISHER = {IEEE}, YEAR = {2023} }
Cyber-Physical Systems (CPSs), i.e., systems comprising both software and physical components, arise in many industry-relevant application domains and 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 (from the user or other systems) and/or of additional, uncontrolled disturbances.
In order 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.
We proposed a technique that, given a collection of scenarios of interest (extracted from mass-storage databases or from symbolic structures like constraint-based scenario generators), computes parallel shortest simulation campaigns (Figure 1), 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, and thus minimising the overall completion time, compatibly with the available simulator memory capacity (Figure 2).


Results
- Experiments on SLV of Modelica/FMU and Simulink case study models with up to almost 200 million scenarios show that optimisation yields speedups as high as 8×
- This, together with the enabled massive parallelisation, makes practically viable (a few weeks in a HPC infrastructure) verification tasks (both statistical and exhaustive, with respect to the given set of scenarios) which would otherwise take inconceivably long time.