Swedish Institute of Computer Science (SICS)
MWB (Mobility WorkBench)
CADP (Construction and Analysis of Distributed Processes)
n/a (the LOTOS description generated a graph of 700,000 states)
The main purpose of a railway signalling system is to prevent
train collisions and derailings while allowing normal train
movement. This study addresses the problem of deciding whether
a given railyard layout and route (settings of points and
signals) is safe, that is, whether trains that respect signals
can move safely.
Each type of component (segment, points, signal) has been modelled as a pi-calculus process. Instances of these processes are then combined to build up the railyard. The desired properties have been expressed in modal mu-calculus and verified (on-the-fly) using the MWB. The railyard specification has also been translated in LOTOS and verified using the EVALUATOR tool from CADP, both on-the-fly and on a minimized graph produced with CAESAR and ALDEBARAN.
All properties except deadlock freedom could be validated with
MWB. Translation to LOTOS proved difficult, but EVALUATOR
could check all properties. We envisage the methods to be
used as a "debugging tool", either for verifying fixed train
routes once and for all or as part of a dynamic control
system. As the number of components increases, state space
explosion has to be tamed: one promising direction for further
work is to explore compositional verification methods.
Lars-åke Fredlund and Fredrik Orava. An experiment in
formalizing and analysing railyard configurations. In
Z. Brezocnik and T. Kapus, editors Proceedings of COST 247
International Workshop on Applied Formal Methods in System
Design (Maribor, Slovenia), pages 51-60. University of
Maribor, Slovenia, June 1996.
Available on-line at:
and from our FTP site in PDF or PostScript
Swedish Institute of Computer Science
S-164 28 KISTA
Tel: +46 8 752 1528
Fax: +46 751 7230
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|