Information Technology Reference
In-Depth Information
Model Checking Interlocking Control Tables
Alessio Ferrari
2
,
1
, Gianluca Magnani
1
,
Daniele Grasso
1
, and Alessandro Fantechi
1
1
University of Florence (DSI)
2
General Electric Transportation Systems (GETS) - Florence
Abstract. A challenging problem for model checking is represented
by railway interlocking systems. It is a well known fact that inter-
locking systems, due to their inherent complexity related to the high
number of variables involved, are not amenable to automatic veri-
fication, typically incurring in state space explosion problems. The
literature is however quite scarce on data concerning the size of in-
terlocking systems that have been successfully proved with model
checking techniques. In this paper we attempt a systematic study of
the applicability bounds for general purpose model checkers on this
class of systems, by studying the typical characteristics of control
tables and their size parameters. The results confirm that, although
small scale interlocking systems can be addressed by model checking,
interlockings that control medium or large railway yards can not,
asking for specialized verification techniques.
Keywords: Railway Interlocking, Model Checking Interlocking, Control
Tables Verification
1
Introduction
In the railway signaling domain, an
interlocking
is the safety-critical sys-
tem that controls the movement of trains in a station and between adjacent
stations. The interlocking monitors the status of the objects in the railway
yard (e.g., points, switches, track circuits) and allows or denies the routing of
trains in accordance with the railway safety and operational regulations that
are generic for the region or country where the interlocking is located. The
instantiation of these rules on a station topology is stored in the part of the
system named
control table
, that is specific for the station where the system
resides [12]. Control tables of modern computerized interlockings are imple-
mented by means of iteratively executed software controls over the status of
the yard objects.
Verification of correctness of control tables has always been a central issue
for formal methods practicioners, and the literature counts the application of
several techniques to the problem, namely the Vienna Development Method
(VDM) [5], property proving [2] [4], Colored Petri Nets (CPN) [1] and model
