RobustRailS
WP 4.1 Formal Development and Verification of Railway Control Systems

Anne E. Haxthausen

DTU Compute, Technical University of Denmark, E-mail: aeha@dtu.dk

This page describes the goals and some of the results achieved in Work Package WP 4.1 of the RobustRailS project.

Goals
Over the next 10 years all Danish railway signalling systems are going to be completely replaced with modern, computer based railway control systems based on the European standard ERTMS/ETCS. The purpose of these systems is to control the railway traffic such that unsafe situations, like train collisions, are avoided. Functional correctness of these new systems is one of the key requisites for a reliable operation of the traffics and in particular for the safety of passengers. Work package 4.1 focuses on how domain-specific techniques and formal development and verification methods can be used for obtaining robust railway control software effectively and efficiently.

Case Study - the Danish Interlocking Systems

WP4.1 has proposed a methodology for automated verification of railway control systems and applied this methodology to a product line of the forthcoming Danish ERTMS level 2 compatible interlocking systems. This has resulted in a domain-specific language and a tool set for formally verifying these systems.

To verify an interlocking system controlling a railway network $N$ using these tools, first the configuration data (including network layouts for $N$ and control tables) for the system is specified in the domain-specific language. Then the tools are used to check that the configuration data are well-formed and to automatically generate (1) a formal, behavioural model $M$ of the system and (2) formal, required safety properties. Finally a bounded model checker is used to automatically check that the model satisfies the safety properties.

The tool set has successfully been applied to formally verify a number of railway networks, including the early deployment line between Roskilde and Næstved.

Some sample railway networks, their XML representation and behavioural models generated from these network representations can be found here: http://www.imm.dtu.dk/ aeha/RobustRailS/data/casestudy

For more information, see [1,2,3,4,5,6], and the following and popularized scientific articles:

• Matematik mindsker risiko for togkollision in Dynamo no 43, 2015. Almost the same text can be found here: Matematik mindsker risiko for togkollision. and in English here: Mathematics reduces the risc of train collisions.
• Matematisk gennembrud øger togsikkerheden/Mathematical breakthrough boosts rail safety in DTUavisen no. 9, 2015
• Rail Safety: Back in the Spotlight in Technologist Magazine, no. 9, pages 42-43, 2016

Case Study - ETCS Ceiling Speed Monitor
See [7,8]. This work has been made in collaboration with the OpenETCS project.

Other Contributions

Development of compositional methods: see [9,10].

Novel concepts of distributed interlocking: see [11,12].

Comparison of formal verification methods for interlocking systems: see [13]. In collaboration with: Hoang Nga Nguyen and Markus Roggenbach.

Contributors to WP4.1

• Anne E. Haxthausen (Work Package Leader of WP 4.1 and Associate Professor at DTU Compute)
• Linh Hong Vu (PhD student at DTU Compute)
• Jan Peleska (Professor at University of Bremen)
• Alessandro Fantechi (as visiting Velux professor at DTU Compute) (is Professor at University of Florence)
• Hugo Macedo (as Postdoc at DTU Compute)
• three assistants and many MSc thesis students

The work has been made in collaboration with Banedanmark and Thales.

Figure: Linh H. Vu and Anne E. Haxthausen, and their collaborator Jan Peleska from Bremen University received the Best-Paper-Award at FORMS/FORMAT 2014 in Braunschweig.

Some useful links:

• - Robustness in Railway Operations.
• DTU Railway Verification Group
• European Technical Working Group on Formal Methods in Railway Control.