Når Banedanmark næste år starter udskiftningen af de gamle signalsystemer, er sikkerheden beregnet på DTU med en helt ny metode.
”Toget er forsinket på grund af en signalfejl”.
Det er en rigtig ærgerlig besked at få fra højtaleren, når man står frysende på en station, og gerne vil hurtigt hjem fra arbejde. Desværre sker det temmelig ofte for de danske togpassagerer, for signalsystemerne er nedslidte og baseret på gammel teknologi. Derfor går Banedanmark nu i gang med en komplet udskiftning af samtlige signaler i hele landet.
Det sker med hjælp fra et hold forskere fra DTU, der har udviklet en metode, der som noget helt nyt matematisk kan bevise sikkerheden for selv meget lange banestrækninger med adskillige stationer. Det har ellers været umuligt, med de metoder man indtil nu har haft til rådighed, fordi computerne løb tør for hukommelse selv ved kortere togstrækninger.
Banedanmark påbegynder udrulningen af de nye signalsystemer i 2016 på strækningen fra Roskilde over Køge til Næstved. Derfor var det netop sikringsanlægget for denne rute, som DTU-forskerne byggede en matematisk model af. Udover at DTU-forskernes model viste, at systemet faktisk virker, og at sikkerheden er i top, så er den nye metode også noget af et matematisk gennembrud.
”Problemet med matematisk at undersøge hver eneste tilstand, som et system kan befinde sig i, er, at det hurtigt bliver utrolig komplekst. Men ved at bruge induktionsbeviser og noget man kalder SMT-baseret modeltjek er det faktisk lykkedes os at verificere en model af en 55 km lang linje med hele otte stationer,” fortæller lektor ved DTU Compute Anne Haxthausen.
Trin for trin
”Kernen i vores metoder er, at vi bruger et værktøj kaldet RT tester til automatisk at udføre induktionsbeviser. Det smarte ved induktionsbeviset er, at man matematisk kan bevise at systemet er sikkert, uden at skulle gennemgå alle systemets mulige tilstande,” forklarer Anne Haxthausen.
Ideen i induktionsbeviset er, at man først beviser, at start-tilstanden er sikker. Derefter ser man kun på overgangen fra en sikker tilstand til den næste, og hvis dette trin også er sikkert, så kan man slutte, at alle tilstande, der kan nås fra starttilstanden og hertil, er sikre. Værktøjet RT tester er udviklet ved Bremens Universitet, men har ikke tidligere været anvendt til induktionsbeviser. Og det er netop denne kombination, som har gjort det muligt at skabe en ny form for verifikationsproces, der har vist sig utrolig effektiv.
”Siden vi for nylig publicerede disse resultater, har vi oplevet en meget stor interesse, fordi resultaterne åbner nye muligheder ikke blot for tjekke sikkerhedskritiske systemer, men også for design og udvikling af nye systemer,” siger Anne Haxthausen.
Matematik er fremtiden
Matematiske metoder er ifølge Anne Haxthausen fremtiden indenfor trafiksystemer, og anbefales stærkt af den europæiske standard for udvikling af software til jernbaneapplikationer.
”At formulere systemegenskaberne i en matematisk model forudsætter at man er 100 procent præcis, og her er matematikken velegnet, da den i modsætning til det almindelige sprog har en fuldstændig utvetydig mening,” siger Anne Haxthausen.
Robustness in Railway OperationS er tværfagligt projekt finansieret af Innovationsfonden. Siden 2012 har forskere fra DTU Management, DTU Transport, DTU Fotonik og DTU Compute arbejdet på at sikre punktlig, pålidelig og sikker togdrift i Danmark i samarbejde med Banedanmark, DSB, DSB S-tog, Trafikstyrelsen, og Bremens Universitet.
Læs evt. mere på: http://www.robustrails.man.dtu.dk/