TY  - JOUR
AU  - Mancini, T.
AU  - Mari, F.
AU  - Massini, A.
AU  - Melatti, I.
AU  - Tronci, E.
PY  - 2021
DA  - 2021//
TI  - On Checking Equivalence of Simulation Scripts
JO  - Journal of Logical and Algebraic Methods in Programming
SP  - 100640
KW  - Formal verification
KW  - Simulation based formal verification
KW  - Formal Verification of cyber-physical systems
KW  - System-level formal verification
AB  - 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.
SN  - 2352-2208
L1  - http://mclab.di.uniroma1.it/publications/papers/mancini/2021/183_Mancini_etal2021.pdf
UR  - http://www.sciencedirect.com/science/article/pii/S2352220821000031
UR  - https://doi.org/10.1016/j.jlamp.2021.100640
DO  - 10.1016/j.jlamp.2021.100640
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=183), last updated on Wed, 20 Jan 2021 09:33:54 +0100
ID  - Mancini_etal2021
ER  -