Click here to flash read.
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
KPIs, when the system runs in its operational environment, i.e., in presence of
inputs (from users or other systems) 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 of interest. Simulation-based SLV can be
computationally prohibitive (years of sequential simulation), since model
simulation is computationally intensive and the set of scenarios of interest
can huge.
We present a technique that, given a collection of scenarios of interest
(extracted from mass-storage databases or from symbolic structures, e.g.,
constraint-based scenario generators), 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 the overall
completion time, compatibly with the available simulator memory capacity.
Our experiments on Modelica/FMU and Simulink case study models with up to
~200 million scenarios show that our optimisation yields speedups as high as
8x. 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.
