Formalising and Analysing Railyard Configurations

Organisation:	Swedish Institute of Computer Science (SICS)
Method:	pi-calculus, LOTOS
Tools used:	MWB (Mobility WorkBench) CADP (Construction and Analysis of Distributed Processes)
Domain:	Railway systems.
Period:	1996
Size:	n/a (the LOTOS description generated a graph of 700,000 states)
Description:	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.
Conclusions:	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.
Publications:	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: http://www.el.feri.uni-mb.si/lms/cost247/proc/orava.ps and from the CADP Web site in PDF or PostScript
Contact:	Lars-åke Fredlund Swedish Institute of Computer Science Box 1263 S-164 28 KISTA SWEDEN Tel: +46 8 752 1528 Fax: +46 751 7230 E-mail: [email protected]
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page