Name
Abstract | ||
|---|---|---|
We show how by combining Explicit Model Checking techniques and simulation it is possible to effectively carry out (bounded) System Level Formal Verification of large Hybrid Systems such as those defined using model-based tools like Simulink. We use an explicit model checker (namely, CMurphi) to generate all possible (finite horizon) simulation scenarios and then optimise the simulation of such scenarios by exploiting the ability of simulators to save and restore visited states. We show feasibility of our approach by presenting experimental results on the verification of the fuel control system example in the Simulink distribution. To the best of our knowledge this is the first time that (exhaustive) verification has been carried out for hybrid systems of such a size. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-39799-8_21 | CAV |
Keywords | Field | DocType |
system level formal verification,hybrid system,model checking,fuel control system example,explicit model checking technique,finite horizon,simulation scenario,large hybrid systems,explicit model checker,simulink distribution | Verification and validation of computer simulation models,Model checking,Computer science,Theoretical computer science,Runtime verification,Control system,High-level verification,Hybrid system,Formal verification,Bounded function | Conference |
Citations | PageRank | References |
23 | 0.73 | 28 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Toni Mancini | 1 | 240 | 25.98 |
| Federico Mari | 2 | 140 | 12.26 |
| Annalisa Massini | 3 | 137 | 15.53 |
| Igor Melatti | 4 | 217 | 19.48 |
| Fabio Merli | 5 | 23 | 0.73 |
| Enrico Tronci | 6 | 336 | 35.83 |