TY  - JOUR
AU  - Mancini, T.
AU  - Mari, F.
AU  - Massini, A.
AU  - Melatti, I.
AU  - Tronci, E.
PY  - 2016//
TI  - Anytime system level verification via parallel random exhaustive hardware in the loop simulation
JO  - Microprocessors and Microsystems
SP  - 12
EP  - 28
VL  - 41
KW  - Model Checking of Hybrid Systems
KW  - Model checking driven simulation
KW  - Hardware in the loop simulation
N2  - 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.
SN  - 0141-9331
UR  - http://www.sciencedirect.com/science/article/pii/S0141933115002045
L1  - papers/mancini/2016/59_Mancini_etal2016.pdf
UR  - http://dx.doi.org/10.1016/j.micpro.2015.10.010
N1  - exported from refbase (show.php?record=59), last updated on Fri, 05 Feb 2016 13:26:29 +0100
ID  - Mancini_etal2016
ER  -