Information Technology Reference
In-Depth Information
naling principles are normally expressed in the principle schemata or in the
regulations. This kind of properties have shown to be representable in Com-
putation Tree Logic (CTL) in the CTL-AGAX form:
AG
, where
p
and
q
are predicates on the variables of our model [6]. CLT-AGAX formulae
have an equivalent Linear Temporal Logic (LTL) representation. The formula
AG
(
p
→
AXq
)
(
p
→
AXq
)
can be expressed in LTL syntax as a LTL-GX formula of the
form
G
. Intuitively, they represent fail-safe conditions, i.e., events
that should happen on the next state if some unsafe condition occurs. One of
the typical safety properties that is normally required to be verified is the
no-
derailing property
: while a train is crossing a point the point shall not change
its position. This typical system level requirement can be easily represented
in the AGAX form [14]:
(
p
→
Xq
)
AG
(
occupied
(
tc
i
)
∧
setting
(
p
i
)=
val
→
AX
(
setting
(
p
i
)=
val
))
whenever the track circuit
tc
i
associated to a point
p
i
is occupied, and the
point has the proper setting
val
, this setting shall remain the same on the
next state.
In order to force the worst-case full state space exploration, our test set
has been designed on purpose to satisfy given properties expressed in CTL-
AGAX (or LTL-GX) form, and model checking has been performed using
these properties as formulae. Though not clearly evident, also for symbolic
model checking we have experienced that satisfied invariants are the hardest
problem.
4
NuSMV
NuSMV is an open-source symbolic model checker that provides the user
with both Binary Decision Diagrams (BDD) based implicit model-checking
and SAT solver based bounded model checking. Properties are encoded in
CTL in the first case, and in LTL in the second case. Since we focus on
the verification of safety properties, we need to be sure that every single
reachable state is analyzed by the model checker; for this reason, we have not
used NuSMV bounded model checking
1
.
In NuSMV, the state is represented by the value of state variables. The
next state is computed by first calculating the next values of state variables
and then, atomically, updating all the state variables. This behaviour of the
model checker is compliant with the chosen model of execution. Every equa-
tion is hence evaluated in sequence but the outputs are updated at the end
of the whole evaluation phase. This behaviour permits to be free from the
order of evaluation of the equations.
NuSMV supports open models, that means that it computes all possible
input variable values automatically: in its internal modeling language the
1
Altough there are techniques that are able to guarantee in some cases the full
exploration of the state space with bounded model checking, these have not been
used in these initial experiments and will be the subject of further experiments.
