Mathematical breakthrough boosts rail safety

"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.

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.

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.