Information Technology Reference
In-Depth Information
keyword IVAR must be used for such variables. Input variables do not con-
tribute to expand the state space of the system, but influence the number
of reachable states. The variables under the keyword VAR are indeed state
variables: the value of each of them in the model is determined by the evalu-
ation of the conditions. In Fig. 1(b) is represented an extract of a NuSMV
model used for our case study.
An example of a CTL-AGAX property that is verified on this SMV model
is: AG(out0=0
→
AX(out1=0)).
5SPIN
SPIN is a generic verification system based on explicit model checking. It
performs a full search in the state-space to find whether or not a given set of
system properties, that are expressed using Linear Temporal Logic (LTL), are
satisfied. The systems are modeled by the verification language PROMELA
(PROcess MEta LAnguage), a C-like language, that provides instruments
especially for the modelling of distributed asynchronous systems.
In this section we will distinguish between input and state variables of the
system that is modeled using PROMELA: this distinction is just conceptual,
since every variable in the model is in fact a state variable. SPIN updates
the state variables on the fly, after the evaluation of the conditions of each
equation; since we want to model a state machine compliant with the cho-
sen execution model, we had to add to the PROMELA model a number of
temporary variables equal to the number of actual state variables, that are
updated only after the evaluations of all the equations, at the end of each
processing step.
A LTL-GX property, corresponding to the CTL-AGAX one given for
NuSMV, that is verified on this PROMELA model is:
X(out1=0)).
An example of model fragment written in PROMELA, corresponding to
the one shown for NuSMV, is represented in Fig. 1(b). Since SPIN can only
verify closed models, we had to model the environment behaviour in the
PROMELA model: in order to model the non-determinism of the input vari-
ables values, we need to insert at the end of the PROMELA model an
if
statement
for each input variable, as represented in the Fig. 1(b).
(out0=0
→
6
Results and Discussion
In order to investigate the actual applicability bounds for the model checking
of interlocking systems, the experiments were performed on generated models
with different equations-inputs ratio. For each combination of inputs and
equations at least three different generic control table models were generated
and tested, in order to be able to avoid erroneous positive results caused
by the generation of trivial equations: if at least one of the three model is
