Simulator Semantics for System Level Formal Verification
Toni Mancini

Federico Mari

Annalisa Massini

Igor Melatti

Enrico Tronci

Computer Science Department - Sapienza University of Rome
Via Salaria 113, I-00198 Roma, Italy
{tmancini,mari,massini,melatti,tronci}@di.uniroma1.it

Many simulation based Bounded Model Checking approaches to System Level Formal Verification (SLFV) have been devised. Typically such approaches exploit the capability of simulators to
save computation time by saving and restoring the state of the system under simulation. However,
even though such approaches aim to (bounded) formal verification, as a matter of fact, the simulator
behaviour is not formally modelled and the proof of correctness of the proposed approaches basically
relies on the intuitive notion of simulator behaviour. This gap makes it hard to check if the optimisations introduced to speed up the simulation do not actually omit checking relevant behaviours of the
system under verification.
The aim of this paper is to fill the above gap by presenting a formal semantics for simulators.

1

Introduction

System Level Verification (SLV) of Cyber-physical Systems has the goal of verifying that the whole (i.e.,
software + hardware) system meets the given specifications. Hardware In the Loop Simulation (HILS)
is currently the main workhorse for system level verification and is supported by Model Based Design
tools such as Simulink, (http://www.mathworks.com) VisSim, (http://www.vissim.com)
and Modelica (https://www.modelica.org/). In HILS the actual software reads [sends] values
from [to] mathematical models (simulation) of the physical systems (e.g. engines, analog circuits, etc.)
it will be interacting with.
Our System Under Verification (SUV) state can take discrete values (e.g., from the software state)
as well as continuous values (e.g., from the physical system state). Thus our SUV can be conveniently
modelled as a Hybrid System (e.g., see [2] and citations thereof) whose inputs belong to a finite set of
uncontrollable events (disturbances) modelling failures in sensors or actuators, variations in the system
parameters, etc.
We focus on deterministic systems (the typical case for control systems), and model nondeterministic
behaviours (such as faults) with disturbances. Accordingly, in our framework, a simulation scenario is
just a finite sequence of disturbances.
A system is expected to withstand all disturbance sequences that may arise in its operational scenarios. Correctness of a system is thus defined with respect to such admissible disturbance sequences and
the goal of HILS is exactly that of showing that indeed the considered SUV can withstand all admissible
disturbance sequences. The set of admissible disturbance sequences typically satisfies constraints like
the following: 1) the number of failures occurring within a certain period of time is less than a given
threshold; 2) the time interval between two consecutive failures is greater than a given threshold; 3) a
failure is repaired within a certain time, etc.
We focus on HILS based Bounded SLFV of safety properties. That is, given a time horizon T and
a time step τ (time quantum between disturbances) our HILS campaign returns PASS if there is no
admissible disturbance sequence of length T and time step τ that violates the property under verification
J. Esparza, E. Tronci (Eds.): Games, Automata,
Logics and Formal Verification 2015 (GandALF’15)
EPTCS 193, 2015, pp. 86–99, doi:10.4204/EPTCS.193.7

T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci

87

and FAIL , along with a counterexample, otherwise. In other words, Bounded SLFV is an exhaustive
(with respect to the set of admissible disturbance sequences) HILS campaign. In such a framework our
exhaustive HILS campaign works as a black box bounded model checker where the SUV behaviour is
defined by a simulator.

1.1

Motivations

In our context the number of admissible disturbance sequences is finite since the number of disturbances
is finite and the time horizon as well as the time quantum between disturbances are both bounded. Nevertheless the number of admissible disturbance sequences can be quite large. As a result, depending on the
system considered and on the degree of assurance sought a HILS campaign may easily require months
of simulation activity.
To decrease such a simulation time many HILS based Bounded Model Checking approaches to SLFV
have been devised. Typically such approaches save simulation time by avoiding simulating more than
once the same sequence of disturbances. This, in turn, is attained by exploiting the capability of simulators to save and restore a simulation state.
However, even though such approaches aim to (bounded) formal verification, as a matter of fact the
simulator behaviour is never formally modelled and the proof of correctness of the proposed approaches
basically relies on the intuitive notion of simulator behaviour. This gap makes it hard to check if the
optimisations introduced to speed up the simulation do not actually omit checking of relevant behaviours
of the system under verification.
The aim of this paper is to fill the above gap by presenting a formal semantics for simulators and by
proving soundness and completeness properties for it.

1.2

Main Contributions

Our main contributions can be summarised as follows.
We give a formal notion of simulator, of simulation campaign, and provide a formal operational
semantics for simulators.
We show soundness of our simulator semantics by showing that any simulation campaign defines a
set of (in silico) experiments that can be carried out on our SUV.
We show completeness of our simulator semantics by showing that any set of (in silico) experiments
to be carried out on our SUV can be defined with a simulation campaign.

1.3

Related Work

SLFV of cyber-physical systems via HILS based bounded model checking has been studied in many
contexts. Here are a few examples. Formal verification of Simulink models has been investigated in [22,
18, 25] focusing on discrete time models (e.g., Stateflow or Simulink restricted to discrete time operators)
with small domain variables. Formal verification of fully general Simulink models has been investigated
in [12, 13, 14, 15]. Formal verification of satellite operational procedures using ESA SIMSAT simulator
has been investigated in [7].
Simulation based approaches to statistical model checking have been widely investigated. Here are
just a few examples: Simulink models for cyber-physical systems have been studied in [28], mixedanalog circuits have been analyzed in [5], smart grid control policies have been considered in [16], and
biological models have been studied in [19, 23, 17].

88

Simulator Semantics for Model Checking Driven Simulation
u(t)

ψ(u,t)
u(t)

(a)

t

SUV

ψ(u,t)

1
0

(b)

(c)

t

≥0

Figure 1: (a) a discrete event sequence u ∈ U R ; (b) our SUV; (c) the SUV output ψ(u,t)

Of course Model Based Testing (e.g., see [4]) has widely considered automatic generation of test
cases from models. In our HILS setting, automatic generation of simulation scenarios (for Simulink) has
been investigated, for example, in [8, 10, 3, 24].
Finally, synergies between simulation and formal methods have been widely investigated also in
digital hardware verification. Examples are in [26, 9, 20, 6] and citations thereof.
All simulation based verification approaches considered in the literature heavily rely on carefully
driving simulators in order to effectively carry out the planned verification activity. However, to the best
of our knowledge, none of them addresses the issue of providing a simulator semantics accounting for the
simulator commands enabling saving and restoring of simulation states (the main simulation commands
used to save simulation time).

1.4

Outline of the paper

Section 2 describes how we model disturbances as uncontrollable inputs to our (cyber-physical) SUV
that, in turn, is modelled as a discrete event system. Section 3 formalises the notion of simulator, simulation campaign and simulator semantics. Section 4 and Section 5 provide, respectively, soundness and
completeness theorems for our simulator semantics.

2

Dynamical Systems

In this section we give the formal background on which our approach rests. To this end, we model disturbances (Definition 1) and define our system (Definition 4), by rephrasing the definition of dynamical
system (see, e.g., [21]). Then, we define the simulation scenario, that is the sequence of disturbances
occurring when the system starts from a given state, and the set of transitions associated to it.
Throughout the paper, we denote N the set of natural numbers, N+ the set of positive natural numbers,
+
R , R≥0 and R the sets of positive, non-negative and all real numbers, respectively. Throughout the
paper, we use R≥0 to represent time and R+ to represent non-zero time durations.
A discrete event sequence (Definition 1 and Figure 1(a)), is a function associating to each (continuous) time instant a disturbance event (such as a fault, a variation in a system parameter, etc). We are
considering a bounded time horizon, accordingly we require that the number of disturbances is finite,
since no system can withstand an infinite number of disturbances within a finite time. We represent with
the real number 0 the event carrying no disturbance and with nonzero reals actual disturbances.
Definition 1 (Discrete event sequence) Let U be a finite subset of R such that 0 ∈ U . A discrete event
sequence over U is a function u : R≥0 → U such that the set {t ∈ R≥0 | u(t) 6= 0} has finite cardinality.
≥0
We denote with U R the set of discrete event sequences over U . We call time horizon of a discrete
event sequence u the value max{t ∈ R≥0 | u(t) 6= 0}.

T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci

89

An event list provides an explicit representation for a discrete event sequence by listing pairs (τ, e),
where e > 0 is an event and τ is the time elapsed since the last (nonzero) event.
Example 1 (Discrete event sequence and event list) As a first example, let us consider the function u
defined as follows:
(
1 for t = kτ, where k = 1, 2, 3 and τ = 1
u(t) =
0 otherwise
The corresponding event list is: [(τ, 1), (τ, 1), (τ, 1)], and the time horizon of u is 3τ.
Remark 1 Let δ (t), with t ∈ R, be the function such that if t = 0 then δ (t) = 1, else δ (t) = 0, that is
δ (t) represents a discrete impulse. Any discrete event sequence u(t) with horizon h can be written in a
unique way as finite sum of discrete impulses, that is:
h

i−1

u(t) = p0 δ (t) + ∑ pi δ (t − ∑ τk )
i=1

k=0

where p0 ∈ U , pi ∈ (U − {0}), and τk ∈ R+ .
Example 2 (Impulses) Let us consider the discrete event sequence u represented in Figure 1(a). It can
be defined using impulses as follows:
u(t) = 2δ (t − 3) + 3δ (t − 5) + δ (t − 10) + 2δ (t − 13)
The event list associated to u is: [(3τ, 2), (2τ, 3), (5τ, 1), (3τ, 2)].
Definition 4 formalizes how we model our SUV, whereas Definition 2 and 3 define, respectively, the
≥0
subset of U R obtained as a restriction to a real interval, and the concatenation of two such subsets.
≥0

Definition 2 Let U R be the set of discrete event sequences over the set U . Given a discrete event
≥0
sequence u ∈ U R and two positive real numbers t1 ≤ t2 , we denote with u |[t1 ,t2 ) the restriction of u to
the interval [t1 ,t2 ), i.e. the function u |[t1 ,t2 ) : [t1 ,t2 ) → U , such that u |[t1 ,t2 ) (t) = u(t) for all t ∈ [t1 ,t2 ).
≥0
We denote U [t1 ,t2 ) the restriction of U R to the domain [t1 ,t2 ).
Definition 3 Assume that t1 ,t2 ,t3 ∈ R≥0 such that t1 < t2 < t3 . If ω ∈ U [t1 ,t2 ) and ω 0 ∈ U [t2 ,t3 ) , their
concatenation, denoted as ωω 0 , is the function ω̃ ∈ U [t1 ,t3 ) defined as:
(
ω(t) if t ∈ [t1 ,t2 )
ω̃(t) =
ω 0 (t) if t ∈ [t2 ,t3 )
In our setting the system to be verified can be modelled as a continuous time Input-State-Output
deterministic dynamical system (see e.g. [21]) whose input functions are discrete event sequences, whose
state can undertake continuous as well as discrete changes, and whose output ranges on any combination
of discrete and continuous values.
Definition 4 (Discrete Event System) A Discrete Event System, or simply DES, H is a tuple
(X , U , Y , ϕ, ψ), where:
• X , the state space of H , is a non-empty set whose elements denote states;
• U , the input value space of H , is a finite subset of R such that 0 ∈ U ;

90

Simulator Semantics for Model Checking Driven Simulation
• Y , the output value space of H , is a non-empty set of outputs;
≥0

• ϕ : R+ × X × U R → X is the transition map of H . Function ϕ must satisfy the following
properties:
– semigroup: for each t1 ,t2 ,t3 ∈ R≥0 such that t1 < t2 < t3 , ω ∈ U [t1 ,t2 ) , ω 0 ∈ U [t2 ,t3 ) , x ∈ X
we have that ωω 0 ∈ U [t1 ,t3 ) is such that ϕ(t3 − t1 , x, ωω 0 ) = ϕ(t3 − t2 , ϕ(t2 − t1 , x, ω), ω 0 );
– consistency: for each u ∈ U , x ∈ X , we have ϕ(0, x, u) = x;
• ψ : R≥0 × X → Y is the observation function of H .
Note that any simulator driven by its script language can be seen as a discrete event system. This is
why we focus on DES.
Our approach can model both the case in which the input is controllable, for example by control
software (Example 3), and the case in which the input is uncontrollable, for example disturbances such
as faults (Examples 4 and 5).
Example 3 (Inverted Pendulum) A simple system is given by the Inverted Pendulum with Stationary
Pivot Point, see e.g. [11, 1]. The system is modeled by taking the angle θ and the angular velocity θ̇ as
state variables. The input of the system is the torquing force u, that can influence the velocity in both
directions. Moreover, the behaviour of the system depends on the pendulum mass m, the length of the
pendulum l and the gravitational acceleration g. Given such parameters, the motion of the system is
described by the differential equation θ̈ = gl sinθ + ml1 2 u.
Let U be {−1, 0, 1}, τ = 10−6 . Our discrete event system H is the tuple (X , U , Y , ϕ, ψ), where:
• X = R2 and Y = R2 ;
• ϕ is solution to the system of differential equations:
x˙1 = x2
x˙2 = gl sinx1 + ml1 2 u
where x1 is the angle θ and x2 is the angular velocity θ̇ ;
• ψ(t) is given by [x1 (t), x2 (t)].
In Figure 2 the Simulink model of the inverted pendulum is shown, where we assume the pendulum
mass m = 1 and the length of the pendulum l = 1. Also we assume the function u is given to the model
as a sequence of values in the set {−1, 0, 1}.
Example 4 (Inverted pendulum on cart) Another example is given by the inverted pendulum on cart.
For this system, the control input is the force F that moves the cart horizontally and the outputs are the
angular position of the pendulum θ and the horizontal position of the cart x. The physical constraint
between the cart and pendulum gives that both the cart and the pendulum have one degree of freedom
each (x and θ , respectively). The controlled system (the plant) consists of the cart and the pendulum,
whereas the controller consists of the control software computing F from the plant outputs (x and θ ). The
dynamics of the system is described in the example available in the Simulink distribution. The Simulink
model of the pendulum on cart, where disturbances are added, is shown in Figure 3.
The system state is a pair (z, w) where z is the state of the control software and w is the plant state,
namely w = [w1 , w2 , w3 , w4 ], where: w1 = cart position, w2 =cart velocity , w3 = pendulum angle, w4 =
pendulum angular velocity.
We model irregularities in the cart rail with a disturbance on the cart weight with respect to its
nominal value 0.455 kg. Let U = {0, 1, 2} be our set of disturbances (see Definition 1) modelling the
fact that the cart weight is (d + 0.455), with d ∈ U .

T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci

91

Figure 2: Simulink model of the inverted pendulum.

We will use the Inverted pendulum on cart (Example 4) as running example throughout the paper.
Example 5 (Fuel Control System) The Fuel Control System (FCS) model in the Simulink distribution
(see Figure 4) has been studied in [27] using statistical model checking techniques, whereas the formal
verification has been discussed in [12, 14]. The model is equipped with four sensors: throttle angle,
speed, Oxygen in Exhaust Gas (EGO) and Manifold Absolute Pressure (MAP). In this case, the tuple
(X , U , Y , ϕ, ψ) representing the discrete event system is:
• X is the set of plant (i.e., the engine) states along with the control software states;
• Y is the set of plant outputs monitored by the control software;
• U is the set of disturbance sequences that can be obtained assuming that only sensors EGO and
MAP can fail, giving rise to disturbances 1 and 2, respectively; the minimum time between faults
is one second and all faults are transient, that is disturbance 1 models a fault on sensor EGO,
followed by a repair within one second, and disturbance 2 models a fault on sensor MAP, followed
by a repair within one second too;
• ϕ computes the dynamics of the system states;
• ψ(t) computes the system output from the present system state.
Our discrete event system as defined in Definition 4, models a hybrid system describing a cyber
physical system, as shown in Examples 3, 4 and 5. For this reason, we denote our system with H .
In the following we define the notion of simulation scenario, that is the sequence of disturbances
received by our system starting from a given initial state, and we give an example.
Definition 5 (Simulation scenario) A simulation scenario for H is a pair (x, u) where x ∈ X and
≥0
u∈UR .
Example 6 (Simulation scenario) Let H be the Inverted pendulum on cart system described in Example 4. Let u(t) be the discrete event sequence defined as: u(t) = δ (t − 0.04) + δ (t − 0.08) and let
the initial state be x0 = (z0 , [0, 0, 0, 0]), where z0 is the control software initial state. Then, a simulation
scenario for H is (x0 , u).
Definitions 6 and 7 give the definition of sequence of transitions and set of transitions explored by a
SUV under a given simulation scenario, respectively.

92

Simulator Semantics for Model Checking Driven Simulation

(a) Inverted pendulum on cart of the Simulink distribution

(b) Cart model with disturbances

Figure 3: Simulink model of the pendulum on cart with disturbances.
≥0

Definition 6 (Trace of a simulation scenario) Let H be a DES and let x ∈ X be a state and u ∈ U R ,
u(t) = p0 δ (t) + ∑hi=1 pi δ (t − ∑i−1
k=0 τk ), a discrete event sequence giving a simulation scenario (x, u)
for H . The trace of the simulation scenario (x, u), denoted Tr(x, u), is the finite sequence of transitions Tr(x, u) = [(x0 , p0 , 0, x1 ), (x1 , p1 , τ1 , x2 ), . . . , (xh−1 , ph−1 , τh−1 , xh )] such that x0 = x and xi+1 =
ϕ(τi , xi , pi δ (t)).
Example 7 (Trace of a simulation scenario) Let H be the Inverted pendulum on cart system described in Example 4 and let (x0 , u) be the simulation scenario of Example 6.
The trace of (x0 , u) is Tr(x0 , u) = [(x0 , 0, 0, x1 ), (x1 , 1, 0.04, x2 ), (x2 , 1, 0.04, x3 )], where x0 =
(z, [0, 0, 0, 0]) and the xi values, i = 1, 2, 3 are obtained by running the simulation with the
Simulink model shown in Example 4 and are: x1 = (z1 , [−0.017, −0.881, 0.057, 2.914]), x2 =
(z2 , [−0.049, −0.694, 0.167, 2.451]) and x3 = (z3 , [−0.072, −0, 431, 0.253, 1.878]).
Definition 7 (Set of transitions of a simulation scenario) The set of transitions associated to a simulation scenario (x, u) is the set:
T(x,u) = {(z, p, τ, z0 )|(z, p, τ, z0 ) ∈ Tr(x, u)}

T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci

93

Figure 4: The Simulink Fuel Control System.

Example 8 (Set of transitions of a simulation scenario) Let us consider system H , simulation scenario (x0 , u), and trace Tr(x0 , u) as in Example 6. The set of transitions associated to (x0 , u) is simply
the set T(x,u) = {(x0 , 0, 0, x1 ), (x1 , 1, 0.04, x2 ), (x2 , 1, 0.04, x3 )}, where x1 , x2 and x3 assume the values
specified in Example 6.

3

Simulators and Simulation Campaigns

In this Section we formalise the notion of discrete event system simulator (Definition 8 and Definition 9),
of simulation campaign (Definition 10) and of set of transitions of a simulation campaign (Definition 12).
In many cases it is necessary to consider a huge number of simulation scenarios for having an exhaustive HILS. The overall number of simulation steps can be prohibitively large if each scenario is
simulated from the initial state of the (SUV) simulator. The definition of set of transitions of a simulation campaign (Definition 12) helps to individuate states necessary to complete the simulation campaign
avoiding to repeat the same sequence of commands several times.
Definition 8 (Discrete Event System Simulator) A Discrete Event System (DES) simulator S is a tuple (H ,W ), where H = (X , U , Y , ϕ, ψ) is a DES and W is a finite set whose elements are called
simulator states. Each w ∈ W is a pair (x, M) where x ∈ X is a state of H and M is a finite subset of
X that models the content of the simulator memory.
Unless otherwise stated, in the following S is a simulator for the DES H as in Definition 8.
Note that, at the beginning the simulator memory contains the initial state x0 of H .
The semantics of simulator commands we use to execute our simulation scenarios, and the transition
function ξ are given in Definition 9.
Definition 9 (Simulator commands and transition function) Let S be a simulator.
• The commands for S are: load(x), store, free(x), run(p,t), where x ∈ X is a state of H , t ∈ R+
is a time duration, and p ∈ U is an event (x,t, p are command arguments).

94

Simulator Semantics for Model Checking Driven Simulation
• The transition function ξ of S , defines how the internal state of the simulator S changes upon
execution of a command. Namely: ξ (x, M, cmd(args)) = (x0 , M 0 ) when the simulator S moves
from internal state (x, M) to state (x0 , M 0 ) upon processing command cmd with arguments args.
For each x ∈ X , function ξ is defined as follows:
–
–
–
–

if x0 ∈ M then ξ (x, M, load(x0 )) = (x0 , M)
if x0 ∈ M then ξ (x, M, free(x0 )) = (x, M \ {x0 })
ξ (x, M, store) = (x, M ∪ {x})
ξ (x, M, run(p, τ)) = (x0 , M), where x0 = ϕ(τ, x, u), where u(t) = pδ (t).

Given a sequence of simulation scenarios, we can build a sequence of commands, simulation campaign, driving the simulator through such scenarios. We define the simulator output sequence as the
sequence of the SUV outputs associated to the simulator states traversed by a simulation campaign.
Conversely, given a simulation campaign, we can compute the sequence of scenarios simulated by it.
These concepts are formalised in Definition 10.
Definition 10 (Simulation campaign and sequence of simulator states) Let S be a simulator and let
ξ be its transition function.
• A simulation campaign for S is a triple Ξ = (x, M, χ) , where x ∈ X , M ⊂ X and χ
is a sequence (possibly empty or infinite) of commands along with their arguments, χ =
cmd0 (args0 ), cmd1 (args1 ), . . .. A simulation campaign consisting of a finite sequence of commands is a finite simulation campaign or a simulation campaign of finite length; the length of
χ = cmd0 (args0 ), . . . , cmdc−1 (argsc−1 ) is c and it is denoted by |χ| = c.
• The sequence of simulator states of S with respect to a simulation campaign Ξ = (x0 , M0 , χ) is
the sequence (x0 , M0 ), (x1 , M1 ), . . ., where for all j, ξ (x j , M j , cmd j (args j )) = (x j+1 , M j+1 ).
We denote with χ(x0 , M0 , j) the j-th element of such a sequence, that is χ(x0 , M0 , j) = (x j , M j ). In
other words χ(x0 , M0 , j) is the simulator state after the execution of the j-th command.
• The set of simulator states with respect to a simulation campaign χ is denoted χ(x0 , M0 ), that is
χ(x0 , M0 ) = {χ(x0 , M0 , j)| j = 0, 1, . . . , |χ| − 1}.
Example 9 (Simulation campaign) Let H be the Inverted pendulum on cart considered in Example 4
and let (x0 , u) be the simulation scenario considered in Example 6, where u(t) = δ (t − 0.04) + δ (t −
0.08).
The simulation campaign Ξ obtained by using this simulation scenario is the triple Ξ = (x0 , {x0 }, χ),
where χ is the sequence of commands χ = (run(0, 0.04), run(1, 0.04), run(1, 0.04)).
The sequence of simulator states with respect to Ξ is:
run(0,0.04)

run(1,0.04)

run(0,0.04)

(x0 , {x0 }) −−−−−−→ (x1 , {x0 }) −−−−−−→ (x2 , {x0 }) −−−−−−→ (x3 , {x0 }).
State values are obtained by running the simulation.
An example of a more complex simulation campaign,Ξ1 , can be obtained by considering the sequence
of simulation scenarios ((x0 , u), (x3 , u1 ), (x3 , u2 ), (x0 , u3 )), where:
u(t) = δ (t − 0.04) + δ (t − 0.08)
u1 (t) = δ (t − 0.04) + δ (t − 0.08) + δ (t − 0.12)
u2 (t) = δ (t − 0.12)
u3 (t) = δ (t − 0.04) + 2δ (t − 0.12) + δ (t − 0.16) + 2δ (t − 0.24).

T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci

0
1

95

0

1

1

1

1

0

1

1

2
1
0

1

0

1
0
2
1

1
1
0

1

0

1

1

0

0

0

1

1

2

2

Figure 6: A graphical representation of
the normal simulation campaign Ξ2 (Example 10).

Figure 5: A graphical representation of
simulation campaign Ξ1 (Example 9).

A graphical representation of simulation campaign Ξ1 is shown in Figure 5, where we see that the
discrete event sequences u(t) and u3 (t) are applied when having state x0 , and sequences u1 and u2 are
applied having state x3 .
The simulation campaign Ξ1 obtained by using the sequence of simulation scenarios above is the
triple Ξ1 = (x0 , {x0 }, χ1 ) , where χ1 is given by the following command sequence:
χ1 = run(0, 0.04), run(1, 0.04), run(1, 0.04), store,
run(1, 0.04), run(1, 0.04), run(1, 0.04), load(x3 ),
run(0, 0.04), run(0, 0.04), run(1, 0.04), free(x3 ),
load(x0 ), run(1, 0.04), run(0, 0.04), run(2, 0.04),
run(1, 0.04), run(0, 0.04), run(2, 0.04)
The sequence of simulator states with respect to Ξ1 is:
(x0 , {x0 })

run(0,0.04)

−−−−−−→
run(1,0.04)

(x3 , {x0 , x3 }) −−−−−−→
run(0,0.04)

(x3 , {x0 , x3 }) −−−−−−→
load(x0 )

(x1 , {x0 })

run(1,0.04)

−−−−−−→
run(1,0.04)

(x4 , {x0 , x3 }) −−−−−−→
run(0,0.04)

(x7 , {x0 , x3 }) −−−−−−→
run(1,0.04)

(x2 , {x0 })

run(1,0.04)

−−−−−−→
run(1,0.04)

(x5 , {x0 , x3 }) −−−−−−→
run(1,0.04)

(x8 , {x0 , x3 }) −−−−−−→

run(0,0.04)

run(2,0.04)

(x3 , {x0 })

store

−−→
load(x3 )

(x6 , {x0 , x3 }) −−−−→
free(x3 )

(x9 , {x0 , x3 }) −−−−→
run(1,0.04)

(x9 , {x0 }) −−−−→ (x0 , {x0 }) −−−−−−→ (x10 , {x0 }) −−−−−−→ (x11 , {x0 }) −−−−−−→ (x12 , {x0 }) −−−−−−→
run(0,0.04)

run(2,0.04)

(x13 , {x0 }) −−−−−−→ (x14 , {x0 }) −−−−−−→ (x15 , {x0 })
Definition 11 gives the notion of normal simulation campaign, that is a simulation campaign for
which every simulation scenario starts from an initial state.
Definition 11 (Normal Simulation Campaign) A simulation campaign is in normal form if it consists
only of commands load and run.
Example 10 (Normal Simulation Campaign) An example of simulation campaign in normal form is
Ξ2 = (x0 , {x0 }, χ2 ), where χ2 is given by the following command sequence:
χ2 = run(0, 0.04), run(1, 0.04), run(1, 0.04), run(1, 0.04), run(1, 0.04), run(1, 0.04),
load(x0 ), run(0, 0.04), run(1, 0.04), run(1, 0.04), run(0, 0.04), run(0, 0.04), run(1, 0.04),
load(x0 ), run(1, 0.04), run(0, 0.04), run(2, 0.04), run(1, 0.04), run(0, 0.04), run(2, 0.04)
A graphical representation of Ξ2 is shown in Figure 6.

96

Simulator Semantics for Model Checking Driven Simulation

Note that, since a normal simulation campaign has no store commands, a command load can only
load an initial state.
Definition 12, resting on Definition 10, defines the set of transitions of a simulation campaign. Definition 13 gives the notion of equivalent simulation campaigns.
Definition 12 (Set of transitions of a Simulation Campaign) We denote with TΞ the set of transitions of S explored by Ξ, that is TΞ = {(x, p, τ, x0 )|∃ M, M 0 [(x, M) is a simulator state of S wrt Ξ ∧
ξ (x, M, run(p, τ)) = (x0 , M 0 )]}.
Definition 13 (Equivalent simulation campaigns) We say that the simulation campaign Ξ is equivalent
to Ξ0 and we write Ξ ∼ Ξ0 if TΞ = TΞ0 .
Example 11 (Equivalent simulation campaigns) The simulation campaign Ξ1 in Example 9 and the
normal simulation campaign Ξ2 in Example 10 are equivalent.
In fact the set of transitions explored by Ξ1 and Ξ2 is:
TΞ1 = TΞ2 = { (x0 , 0, 0.04, x1 ), (x1 , 1, 0.04, x2 ), (x2 , 1, 0.04, x3 ), (x3 , 1, 0.04, x4 ), (x4 , 1, 0.04, x5 ),
(x5 , 1, 0.04, x6 ), (x3 , 0, 0.04, x7 ), (x7 , 0, 0.04, x8 ), (x8 , 1, 0.04, x9 ), (x0 , 1, 0.04, x10 ), (x10 , 0, 0.04, x11 ),
(x11 , 2, 0.04, x12 ), (x12 , 1, 0.04, x13 ), (x13 , 0, 0.04, x14 ), (x14 , 2, 0.04, x15 )}
This can also be easily seen looking at the set of edges (transitions) in Figures 5 and 6.
Lemma 1 formalizes the fact that for each simulation campaign, we can determine an equivalent
simulation campaign in which each simulation scenario starts from an initial state.
Lemma 1 Given a simulation campaign Ξ for a simulator S , there exists a simulation campaign Ξ0
such that:
• Ξ0 is in normal form
• Ξ0 ∼ Ξ
We give the idea of the proof by using the following example.
Example 12 (Lemma 1) Consider the simulation campaign Ξ1 in Example 9. Ξ1 is not in normal form.
However, by modifying it so that all simulation scenarios (paths on the tree of Figure 5) start from the
initial state, we get the normal simulation campaign Ξ2 illustrated in Example 10.
Further, it follows from Example 10 that Ξ1 ∼ Ξ2 .

4

Soundness

In this section we show the soundness of our simulator semantics. That is, we show that any simulation
campaign stems from a set of simulation scenarios. This guarantees that any simulation campaign has
indeed a physical (computational) meaning.
Theorem 1 (Soundness) Given a simulation campaign Ξ for S
{(x1 , u1 ), (x2 , u2 ), . . . , (xk , uk )} of simulation scenarios such that

there exists a set A =

TΞ = ∪{T(xi ,ui ) | i = 1, . . . , k}.
As we did for Lemma 1, we give the idea of the proof by using an example.

T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci

97

Example 13 (Soundness) Consider the simulation campaign Ξ1 in Example 9. The set of transitions of
Ξ1 , TΞ1 , is shown in Example 11.
Now, let us consider the set A consisting of simulation scenarios (x0 , u), (x3 , u1 ), (x3 , u2 ) and
(x0 , u3 ), defined in Example 9.
The sets of transitions for simulation scenario (x0 , u) is shown in Example 8, and the sets of transitions associated to the other three simulation scenarios are, respectively:
T1 = T(x3 ,u1 ) = { (x3 , 1, 0.04, x4 ), (x4 , 1, 0.04, x5 ), (x5 , 1, 0.04, x6 )}
T2 = T(x3 ,u2 ) = { (x3 , 0, 0.04, x7 ), (x7 , 0, 0.04, x8 ), (x8 , 1, 0.04, x9 )}
T3 = T(x0 ,u3 ) = { (x0 , 1, 0.04, x10 ), (x10 , 0, 0.04, x11 ), (x11 , 2, 0.04, x12 ), (x12 , 1, 0.04, x13 ),
(x13 , 0, 0.04, x14 ), (x14 , 2, 0.04, x15 )}
It is easy to see that TΞ1 = ∪{T j | j = 0, . . . , 3}.

5

Completeness

In this section we show the completeness of our simulator semantics. That is, we show that any set of
simulation scenarios yields a simulation campaign. This guarantees that any set of physical experiments
can be defined by a suitable simulation campaign.
Theorem 2 Let A = {(x1 , u1 ), (x2 , u2 ), . . . , (xk , uk )} be a set of simulation scenarios of H . Then there
exists a simulation campaign Ξ for S such that
TΞ = ∪{T(xi ,ui ) | i = 1, . . . , k}.
Also for this theorem, we give the idea of the proof by using an example.
Example 14 (Completeness) Let us consider the set A consisting of simulation scenarios (x0 , u),
(x3 , u1 ), (x3 , u2 ) and (x0 , u3 ), defined in Example 9.
The sets of transitions associated to these simulation scenarios, T0 = T(x0 ,u) , T1 = T(x3 ,u1 ) , T2 =
T(x3 ,u2 ) and T3 = T(x0 ,u3 ) , are shown in Example 13. Let T¯ be the set obtained as union of the sets of
transitions above, that is T¯ = ∪{T j | j = 0, . . . , 3}.
Now, let us consider the simulation campaign Ξ1 in Example 9 and the set of transitions of Ξ1 , TΞ1 ,
shown in Example 11.
It is easy to see that T¯ = TΞ1 .

6

Conclusions

We provided a formal notion of simulator, of simulation campaign. and a formal operational semantics
for simulators.
Furthermore we showed soundness and completeness of our simulator semantics by showing that any
simulation campaign defines a set of (in silico) experiments for the SUV (soundness) and, conversely,
that any such a set can be defined with a simulation campaign (completeness).
This work enables formal proofs of correctness for simulation based formal verification approaches
and provides formal tools enabling investigation of more aggressive approaches to the optimisation of
the simulation activity entailed by HILS based SLFV.
Acknowledgements.
(600773).

Work partially supported by FP7 projects SmartHG (317761) and PAEON

98

Simulator Semantics for Model Checking Driven Simulation

References
[1] V. Alimguzhin, F. Mari, I. Melatti, I. Salvo & E.Tronci (2012): Automatic control software synthesis for
quantized discrete time hybrid systems. In: Proc. 51th IEEE Conference on Decision and Control, CDC,
doi:10.1109/CDC.2012.6426260.
[2] R. Alur (2011): Formal verification of hybrid systems. In: Proc. 11th Int. Conf. on Embedded Software,
EMSOFT 2011, part of the Seventh Embedded Systems Week, ACM, doi:10.1145/2038642.2038685.
[3] A. Brillout, N. He, M. Mazzucchi, M. Purandare D. Kroening, P. Rümmer & G. Weissenbacher (2010):
Mutation-based Test Case Generation for Simulink Models. In: Proc. 8th Int. Conf. on Formal Methods for
Components and Objects, FMCO’09, Springer-Verlag, doi:10.1007/978-3-642-17071-3.
[4] M. Broy, B. Jonsson, J.-P. Katoen, M. Leucker & A. Pretschner (2005): Model-Based Testing of Reactive
Systems: Advanced Lectures. LNCS 3472, Springer, doi:10.1007/b137241.
[5] E. M. Clarke, A. Donzé & A. Legay (2010): On simulation-based probabilistic model checking of mixedanalog circuits. Formal Methods in System Design 36(2), doi:10.1007/s10703-009-0076-y.
[6] F. M. De Paula & A. J. Hu (2007): An effective guidance strategy for abstraction-guided simulation. In: Proc. 44th annual Design Automation Conference, DAC ’07, ACM, New York, NY, USA,
doi:10.1145/1278480.1278498.
[7] Verzino G., F. Cavaliere, F. Mari, I. Melatti, G. Minei, I. Salvo, Y. Yushtein & E. Tronci (2012): Model
checking driven simulation of sat procedures. In: Proc. of 12th International Conference on Space Operations
(SpaceOps 2012), SpaceOps, doi:10.2514/6.2012-1275611.
[8] A. A. Gadkari, A. Yeolekar, J. Suresh, S. Ramesh, S. Mohalik & K. C. Shashidhar (2008): AutoMOTGen:
Automatic Model Oriented Test Generator for Embedded Control Systems. In: Proc. 20th Int. Conf. Computer
Aided Verification, CAV, doi:10.1007/978-3-540-70545-1 19.
[9] P. H. Ho, T. Shiple, K. Harer, J. Kukula, R. Damiano, V. Bertacco, J. Taylor & J. Long (2000): Smart
simulation using collaborative formal and simulation engines. In: Proc. 2000 IEEE/ACM Int. Conf. on
Computer-aided design, ICCAD ’00, IEEE Press, doi:10.1109/ICCAD.2000.896461.
[10] A. Kanade, R. Alur, F. Ivancic, S. Ramesh, S. Sankaranarayanan & K. C. Shashidhar (2009): Generating
and Analyzing Symbolic Traces of Simulink/Stateflow Models. In: Proc. 21st Int. Conf. Computer Aided
Verification, CAV, doi:10.1007/978-3-642-02658-4 33.
[11] G. Kreisselmeier & T. Birkholzer (1994): Numerical nonlinear regulator design. Automatic Control, IEEE
Transactions on 39(1), doi:10.1109/9.273337.
[12] T. Mancini, F. Mari, A. Massini, I. Melatti, F. Merli & E. Tronci (2013): System Level Formal Verification
via Model Checking Driven Simulation. In: Computer Aided Verification - 25th International Conference,
CAV, doi:10.1007/978-3-642-39799-8 21.
[13] T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci (2014): Anytime System Level Verification via Random
Exhaustive Hardware in the Loop Simulation. In: 17th Euromicro Conference on Digital System Design,
DSD, doi:10.1109/DSD.2014.91.
[14] T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci (2014): System Level Formal Verification via Distributed Multi-core Hardware in the Loop Simulation. In: 22nd Euromicro International Conference on
Parallel, Distributed, and Network-Based Processing, PDP, doi:10.1109/PDP.2014.32.
[15] T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci (2015): SyLVaaS: System Level Formal Verification
as a Service. In: 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based
Processing, PDP, doi:10.1109/PDP.2015.119.
[16] T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. K. Gruber, B. Hayes, M. Prodanovic
& L. Elmegaard (2014): Demand-aware price policy synthesis and verification services for Smart
Grids. In: 2014 IEEE International Conference on Smart Grid Communications, SmartGridComm,
doi:10.1109/SmartGridComm.2014.7007745.

T. Mancini, F. Mari, A. Massini, I. Melatti & E. Tronci

99

[17] T. Mancini, E. Tronci, I. Salvo, F. Mari, A. Massini & I. Melatti (2015): Computing Biological Model
Parameters by Parallel Statistical Model Checking. In: Proc. Third Int. Conf. Bioinformatics and Biomedical
Engineering, IWBBIO, doi:10.1007/978-3-319-16480-9 52.
[18] B. Meenakshi, A. Bhatnagar & S. Roy (2006): Tool for Translating Simulink Models into Input Language of a
Model Checker. In: Proc. 8th Int. Conf. on Formal Engineering Methods, ICFEM, doi:10.1007/11901433 33.
[19] N. Miskov-Zivanov, P. Zuliani, E. M. Clarke & J. R. Faeder (2013): Studies of biological networks with
statistical model checking: application to immune system cells. In: ACM Conference on Bioinformatics,
Computational Biology and Biomedical Informatics. ACM-BCB, doi:10.1145/2506583.2512390.
[20] K. Nanshi & F. Somenzi (2006): Guiding simulation with increasingly refined abstract traces.
In: Proc. 43rd annual Design Automation Conference, DAC ’06, ACM, New York, NY, USA,
doi:10.1145/1146909.1147097.
[21] E.D. Sontag (1998): Mathematical Control Theory: Deterministic Finite Dimensional Systems. Texts in
Applied Mathematics, Springer, doi:10.1007/978-1-4612-0577-7.
[22] S. Tripakis, C. Sofronis, P. Caspi & A. Curic (2005): Translating discrete-time simulink to lustre. ACM
Trans. Embedded Comput. Syst. 4(4), doi:10.1145/1113830.1113834.
[23] E. Tronci, T. Mancini, I. Salvo, S. Sinisi, F. Mari, I. Melatti, A. Massini, F. Davi, T. Dierkes, R. Ehrig,
S. Röblitz, B. Leeners, T. H. C. Kruger, M. Egli & F. Ille (2014): Patient-specific models from interpatient biological models and clinical records. In: Formal Methods in Computer-Aided Design, FMCAD,
doi:10.1109/FMCAD.2014.6987615.
[24] R. Venkatesh, U. Shrotri, P. Darke & P. Bokil (2012): Test generation for large automotive models. In: IEEE
Int. Conf. on Industrial Technology (ICIT), doi:10.1109/ICIT.2012.6210014.
[25] M. W. Whalen, D. D. Cofer, S. P. Miller, B. H. Krogh & W. Storm (2007): Integration of Formal Analysis into
a Model-Based Software Development Process. In: Proc. 12th Int. Workshop Formal Methods for Industrial
Critical Systems, FMICS, doi:10.1007/978-3-540-79707-4 7.
[26] C. H. Yang & D. L. Dill (1998): Validation with guided search of the state space. In: Proc. 35th annual
Design Automation Conference, DAC ’98, ACM, New York, NY, USA, doi:10.1145/277044.277201.
[27] P. Zuliani, A. Platzer & E. M. Clarke (2010): Bayesian statistical model checking with application to
Simulink/Stateflow verification. In: Proc. 13th ACM Int. Conf. on Hybrid Systems: Computation and Control,
HSCC, doi:10.1145/1755952.1755987.
[28] P. Zuliani, A. Platzer & E. M. Clarke (2013): Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods in System Design 43(2), doi:10.1007/s10703-013-0195-3.

