Information Technology Reference
In-Depth Information
checking [14] [10] [11]. This last technique in particular has raised the inter-
est of many railway signaling industries, being the most lightweight from the
process point of view, and being rather promising in terms of eciency. Nev-
ertheless, application of model cheking for the verification of safety properties
has been successfully performed only on small case studies, often requiring
the application of domain-related heuristics based on topology decomposi-
tion. The literature is however quite scarce on data concerning the size of
interlocking systems that have been successfully proved with model checking
techniques. This is partly due to confidentiality reasons, and partly to the
fact that the reported experiences refer to specific case studies, with a limited
possibility of scaling the obtained results to larger systems.
We have therefore decided to investigate more systematically the actual
applicability bounds for widely used model checkers on this class of systems,
by studying the typical characteristics of control tables and their size pa-
rameters. In particular, we have chosen to compare the performances of two
popular general purpose model checkers, the symbolic model checker NuSMV
[3] and the explicit model checker SPIN [8]. A test set of generic control table
models of increasing complexity has been defined and translated into the in-
put language of the two tools, and generic safety properties have been proved
on them by the two model checkers. The results have confirmed that the
bound on the size of the controlled yard that can be safely addressed by the
two tools is still rather small, making general purpose model checking tools
not usable for medium and large scale interlockings. Specifically optimized
verification techniques should be studied to allow the verification of such
complex systems.
2
Interlocking Systems Representation
In Relay Interlocking Systems (RIS), currently installed and operating in sev-
eral sites, the logical rules of the control tables were implemented by means
of physical relay connections. With Computer Interlocking Systems (CIS), in
application since 30 years, the control table becomes a set of software equa-
tions that are executed by the interlocking. Since the signaling regulations
of the various countries were already defined in graphical form for the RIS,
and also in order to facilitate the representation of control tables by signal-
ing engineers, the design of CIS has usually adopted traditional graphical
representations such as ladder logic diagrams [4] [9] and relay diagrams [7].
These graphical schemas, usually called
principle schemata
, are instantiated
on a station topology to build the control table that is then translated into
a program for the interlocking.
As pointed out in [4], the graphical representations and the related control
tables can be reduced to a set of boolean equations of the form
x
i
:=
x
j
∧
...
x
. The
variables represent the possible states of the signalling elements monitored by
the control table: system input, output or temporary variables. The equations
∧
x
j
+
k
, where
x
j
...x
j
+
k
are boolean variables in the form
x
or
¬
