Techniques for modelling and verifying railway interlockings

James, Phillip; Moller, Faron; Nguyen, Hoang; Roggenbach, Markus; Schneider, Steve; Treharne, Helen
November 2014
International Journal on Software Tools for Technology Transfer;Nov2014, Vol. 16 Issue 6, p685
Academic Journal
We describe a novel framework for modelling railway interlockings which has been developed in conjunction with railway engineers. The modelling language used is CSP $$||$$ B. Beyond the modelling we present a variety of abstraction techniques which make the analysis of medium- to large-scale networks feasible. The paper notably introduces a covering technique that allows railway scheme plans to be decomposed into a set of smaller scheme plans. The finitisation and topological abstraction techniques are extended from previous work and are given formal foundations. All three techniques are applicable to other modelling frameworks besides CSP $$||$$ B. Being able to apply abstractions and simplifications on the domain model before performing model checking is the key strength of our approach. We demonstrate the use of the framework on a real-life, medium-size scheme plan.


Related Articles

  • Automated generation of formal safety conditions from railway interlocking tables. Haxthausen, Anne // International Journal on Software Tools for Technology Transfer;Nov2014, Vol. 16 Issue 6, p713 

    This paper describes a tool for extracting formal safety conditions from interlocking tables for railway interlocking systems. The tool has been applied to generate safety conditions for the interlocking system at Stenstrup station in Denmark, and the SAL model checker tool has been used to...

  • Dual signalling eases ERTMS roll-out. Utberg, Xaf; Oonincx, Jan // Railway Gazette International;Sep2007, Vol. 163 Issue 9, p570 

    The article reports on the installation of dual signalling system European Train Control System (ETCS) Level 2 and Automatic Train Protection for the Amsterdam--Utrecht main line of ProRail in the Netherlands. It states that the installation of the system will allow the line to be used by both...

  • From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions. Ferrari, Alessio; Spagnolo, Giorgio; Martelli, Giacomo; Menabeni, Simone // International Journal on Software Tools for Technology Transfer;Nov2014, Vol. 16 Issue 6, p647 

    Communications-based train control (CBTC) systems are the new frontier of automated train control and operation. Currently developed CBTC platforms are actually very complex systems including several functionalities, and every installed system, developed by a different company, varies in extent,...

  • Interlocking and Train Protection. Macfarlane, Ian // Railway Gazette International;Oct2004, Vol. 160 Issue 10, p716 

    The article offers information on the book "Interlocking and Train Protection," by Ian Macfarlane. Starting with a vivid description of the head-on collision at Harvey, near Chicago, in 1979, the book contains 13 chapters. It traces the development of interlocking and train control technologies...

  • Definition of the Basic Aspects by Development of Universal Interfaces Between Relay and Microprocessor Systems. Mezitis, Mareks; Kamenevs, Olegs // Transport & Engineering;2009, Vol. 32, p111 

    Represented interface model give a possibility to make interconnection between microprocessors interlocking and Auto Block systems. With in interface model will be kept all functional interdependences and safety level. Absence of running cost for interface integration to Auto Block has positive...

  • End of the line.  // Railway Gazette International;Aug2010, Vol. 166 Issue 8, p71 

    The article reports that the purely mechanical interlockings are no longer used on the U.S. main rail network, after over 150 years of operation.

  • The Design and Implementation of Data Independence in the CSP Model of Security Protocol. Jing An; Lei Zhang; Chunlan You // Advanced Materials Research;2014, Issue 915-916, p1386 

    The CSP method has been extremely effective in checking for, and finding, attacks on security protocol. On the other hand, it has been limited to showing that a given small instance, usually restricted by the finiteness of some set of resources, is free of attacks. In order to resolve this...

  • Optimizing the fleet.  // Railway Age;Dec2004, Vol. 205 Issue 12, p25 

    Focuses on the efforts of the mechanical department of Canadian Pacific Railway (CPR) in optimizing its fleet. Standardization of motive power and rolling stock of CPR; Advantage of the computerized Train Area Marshalling program to the company; Details of the MaxStax program.

  • Modeling and Application of Railway Safety System through Object Petri Nets. Zhang Ye; Jia Limin; Cai Guoqiang // International MultiConference of Engineers & Computer Scientists;2007, p2173 

    The management of railway safety system needs extended and integrated approaches of behavioral characteristics modeling. While most formal approaches to railway safety system modeling consider only the control-flow perspective, it is essential in a function-resource organizational context to...


Other Topics