Mathematics reduces risk of train collision

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