Title
On minimising the maximum expected verification time.
Abstract
Cyber Physical Systems (CPSs) consist of hardware and software components. To verify that the whole (i.e., software + hardware) system meets the given specifications, exhaustive simulation-based approaches (Hardware In the Loop Simulation, HILS) can be effectively used by first generating all relevant simulation scenarios (i.e., sequences of disturbances) and then actually simulating all of them (verification phase). When considering the whole verification activity, we see that the above mentioned verification phase is repeated until no error is found. Accordingly, in order to minimise the time taken by the whole verification activity, in each verification phase we should, ideally, start by simulating scenarios witnessing errors (counterexamples). Of course, to know beforehand the set of such scenarios is not feasible. In this paper we show how to select scenarios so as to minimise the Worst Case Expected Verification Time. Simulation: main workhorse for System Level Verification of Cyber Physical Systems.A counterexample is a simulation scenario witnessing a design error.WCEVT: max expected number of scenarios simulated before hitting a counterexample.We show that the minimum WCEVT is (n+1)/2 (n number of simulation scenarios).The infinite set of optimal simulation strategies forms a convex bounded polytope.
Year
DOI
Venue
2017
10.1016/j.ipl.2017.02.001
Inf. Process. Lett.
Keywords
Field
DocType
Formal verification,Explicit model checking,System-level formal verification,Formal methods,Software engineering
Verification and validation of computer simulation models,Functional verification,Computer science,Simulation,Intelligent verification,Physical verification,Runtime verification,Logic simulation,High-level verification,Software verification
Journal
Volume
Issue
ISSN
122
C
0020-0190
Citations 
PageRank 
References 
3
0.37
32
Authors
6
Name
Order
Citations
PageRank
Toni Mancini124025.98
Federico Mari214012.26
Annalisa Massini313715.53
Igor Melatti421719.48
Ivano Salvo514014.70
Enrico Tronci633635.83