Mathematics reduces risk of train collision

Monday 18 May 15
by Iben Julie Schmidt


Anne Elisabeth Haxthausen
Associate Professor
DTU Compute
+45 45 25 75 10

Banedanmark's signalling programme

Banedanmark is in the process of replacing all outdated Danish signalling systems: Banedanmark's signalling programme. On long-distance lines, tomorrow's signalling system will be the joint European ERTMS 2 system—and on the S-train network a CBTC system.

The new signals will significantly reduce delays, higher speed on certain routes and more trains. The DKK 20-billion replacement of the signalling systems will take place from 2016 to 2021. Fortunately, Banedanmark can draw on state-of-the-art research from DTU thanks to a major research project called RobustRailS.


Robustness in Railway OperationS is large interdisciplinary project funded by the Danish Council for Strategic Research. Since 2012, researchers from DTU Management Engineering, DTU Transport, DTU Fotonik, and DTU Compute have worked on developing new methods for ensuring punctual, safe, and reliable rail services in Denmark in collaboration with Banedanmark, DSB, DSB S-tog, the Danish Transport Authority, and the University of Bremen.

Read more about the project

When Rail Net Denmark (Banedanmark) next year starts replacing obsolete signalling systems with new technology, a new type of safety calculation will be employed. Mathematical methods developed at DTU Compute make it possible to increase the safety level on the Danish rail lines. 

"The train is delayed due to a signal fault." Not what you want to hear when waiting for the train on a cold day, going home from work. But because the signalling systems are old, worn down and based on obsolete technology, this unfortunately happens quite frequently for Danish train passengers.  Therefore, Rail Net Denmark (Banedanmark) now starts replacing all signals across Denmark. The well-known flashing railway signals will disappear. Instead, the signals will be displayed on the engine driver's computer screen.

Safety testing
The purpose of the new signals is not just to reduce the number of delays, but also to enable increasing the number of trains and their speed and, not least, improving safety.
And safety in particular has been a key focus area for the research team at DTU Compute which—in collaboration with, among others, Banedanmark, and the University of Bremen—has developed a new mathematical method for testing the safety of the new systems. The project is part of a large interdisciplinary research project called RobustRailS, funded by the Danish Council for Strategic Research.

"The new signalling system consists of highly complex software systems. And we have examined how mathematical methods enable you to check whether the systems actually work as they should. To this end, we have decided to focus on the most safety-critical element: the safety system intended to prevent train collision and derailment," says Anne Haxthausen, Associate Professor at DTU Compute.

Eliminating dangerous situations
The safety system will, for example, reserve routes for the trains, control track switches, and issue train driving permissions. The Danish long-distance railway network consists of 32 safety systems, each controlling a specific part of the network, for example a major train station or a section with several stations. The new mathematical tool developed at DTU Compute allows you to draw the part of the railway network that is controlled by a safety system in an editor, and a mathematical model of the system is then generated automatically as well as a model of the safety requirements that apply, for example that two trains must never be on the same section simultaneously. And that the position of the track switch must never be changed when a train is passing it. Another tool then checks that the safety requirements are always met, regardless of system mode.

Mathematical breakthrough
DTU researchers have now tested the method which has proved to be something of a mathematical breakthrough:

"The problem of testing each and every system mode mathematically is that it will soon prove extremely complex. Up until now, it has therefore only been possible to test minor parts of a network. As soon as you have tried to test long sections, the computer has run out of memory. But by using induction proofs and something called SMT-based model checking, we have actually succeeded in modelling a 55-kilometre line with no less than eight stations. In addition, the results open up new possibilities—not just for testing safety-critical systems, but also for designing and developing new systems. Because one of the advantages of using the method is that—in principle—you can formulate a model and test the entire system before you actually develop the software," explains Anne Haxthausen, and continues:

"There is no doubt that mathematical methods are the future of traffic systems. The European standard (CENELEC EN 50128) for the development of software for rail applications strongly recommends that you use mathematical methods, because it improves safety. To formulate the system properties in a mathematical model also assumes that you are 100 per cent accurate; and to this end, mathematics is well suited as it, unlike ordinary language, is completely unambiguous," says Anne Haxthausen.