Abstract: To support Model Based Design of Cyber-Physical Systems (CPSs) many simulation based approaches to System Level Formal Verification (SLFV) have been devised. Basically, these are Bounded Model Checking approaches (since simulation horizon is of course bounded) relying on simulators to compute the system dynamics and thereby verify the given system properties. The main obstacle to simulation based SLFV is the large number of simulation scenarios to be considered and thus the huge amount of simulation time needed to complete the verification task. To save on computation time, simulation based SLFV approaches exploit the capability of simulators to save and restore simulation states. Essentially, such a time saving is obtained by optimising the simulation script defining the simulation activity needed to carry out the verification task. Although such approaches aim to (bounded) formal verification, as a matter of fact, the proof of correctness of the methods to optimise simulation scripts basically relies on an intuitive semantics for simulation scripting languages. This hampers the possibility of formally showing that the optimisations introduced to speed up the simulation activity do not actually omit checking of relevant behaviours for the system under verification. The aim of this paper is to fill the above gap by presenting an operational semantics for simulation scripting languages and by proving soundness and completeness properties for it. This, in turn, enables formal proofs of equivalence between unoptimised and optimised simulation scripts.

Abstract: Abstract System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability.