Photo: Colourbox

Mathematical breakthrough boosts rail safety

Tuesday 01 Dec 15
by Iben Julie Schmidt


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


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 been working to ensure punctual, safe, and reliable rail services in Denmark in collaboration with Rail Net Denmark, the Danish National Railways (DSB), DSB S-tog, the Danish Transport Authority, and the University of Bremen. 

When Rail Net Denmark (Banedanmark) starts replacing its old signal systems next year, safety levels will have been calculated at DTU using a completely new method.

"The train is delayed due to a signal fault."

This is not exactly what you want to hear on your way home from work, as you stand waiting for the train on a cold, wet platform. Unfortunately, it is a problem Danish passengers encounter quite frequently because the Danish railway’s signalling systems are old, run down and based on obsolete technology. Rail Net Denmark (Banedanmark) is therefore now starting work on replacing all signals throughout Denmark.

To assist with the work, the organization has called in a team of researchers from DTU, who have developed a completely new method that can mathematically prove the safety of even long stretches of tracks featuring multiple stations. This was otherwise impossible using the methods available to date, because the calculations involved for even short stretches of tracks quickly exhausted the computers’ memories.

Rail Network Denmark will commence rolling out its new signalling systems in 2016, starting with the line running from Roskilde to Næstved via Køge. The DTU researchers therefore constructed their first mathematical model for the safety system used on this route. Over and above demonstrating that the system actually works—and that the safety level is excellent—the DTU researchers’ model also proved that the new method represents an authentic mathematical breakthrough.

“The problem with mathematically testing the status of each and every system is that this approach soon becomes extremely complex. However, by using induction proofs and what is known as ‘SMT-based model checking’, we actually succeeded in verifying a model of a 55-km-long stretch of tracks with no fewer than eight stations,” relates Anne Haxthausen, Associate Professor at DTU Compute.

Photo: Colourbox

Step by step
“The core of our method is our use of a tool called an ‘RT tester’ to perform induction proofs automatically. What is so clever about an induction proof is that it enables us to prove mathematically that the system is safe without having to review all the possible system statuses one by one,” explains Anne Haxthausen.

"Formulating the system properties in a mathematical model assumes 100 per cent accuracy,"
Anne Haxthausen, associate professor at DTU Compute.

The idea behind using induction proofs is that the first step is to prove that the starting status is safe. It is then only necessary to check the transition from one safe status to the next, and if this step is also safe, then it can be concluded that all the intermediate statuses are safe as well. The RT tester tool was developed at the University of Bremen, but it has not previously been used for induction proofs. And it is precisely this combination, which has allowed the development of a new form of verification process, that has proved to be remarkably effective.

“We recently published these findings, and since then we have noted a significant upswing in interest because they open up new opportunities not only for checking systems critical to safety, but also for designing and developing new systems,” says Anne Haxthausen. 

Mathematics is the future
According to Anne Haxthausen, mathematical methods are the future as regards traffic systems, and they are strongly recommended by the European standard for the development of software for railway applications.

“Formulating the system properties in a mathematical model assumes 100 per cent accuracy, and mathematics is extremely well suited to this purpose because, unlike ‘ordinary’ language, it is completely unambiguous,” concludes Anne Haxthausen. 

Article in DTUavisen no. 9, November 2015.

Facts about the project:

Photo: Colourbox  

Rail Net Denmark’s signal programme is set to introduce the signal system of the future—the pan-European ERTMS 2—on its long-distance lines, combined with a CBTC system on the commuter rail routes.


The new signals should significantly reduce delays and allow more trains and faster speeds on some stretches of track.


Replacement of the signal systems is scheduled to run from 2016 to 2021, and the programme is likely to cost more than DKK 20 billion.