On Checking Equivalence of Simulation Scripts
Mancini
T.
author
Mari
F.
author
Massini
A.
author
Melatti
I.
author
Tronci
E.
author
2021
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.
Formal verification
Simulation based formal verification
Formal Verification of cyber-physical systems
System-level formal verification
exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=183), last updated on Wed, 20 Jan 2021 09:33:54 +0100
text
http://www.sciencedirect.com/science/article/pii/S2352220821000031
http://mclab.di.uniroma1.it/publications/papers/mancini/2021/183_Mancini_etal2021.pdf
http://www.sciencedirect.com/science/article/pii/S2352220821000031
10.1016/j.jlamp.2021.100640
Mancini_etal2021
MCLab @ davi @ Mancini2021100640
Journal of Logical and Algebraic Methods in Programming
2021
continuing
periodical
academic journal
100640
2352-2208