On checking equivalence of simulation scripts

摘要

To supportModel Based DesignofCyber-Physical Systems(CPSs) manysimulation basedapproaches toSystem Level Formal Verification(SLFV) have been devised. Basically, these areBounded Model Checkingapproaches (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 ofsimulation scenariosto 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 tosaveandrestoresimulation states. Essentially, such a time saving is obtained byoptimisingthe 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 anoperational semanticsfor simulation scripting languages and by provingsoundnessandcompletenessproperties for it. This, in turn, enables formal proofs ofequivalencebetween unoptimised and optimised simulation scripts.