Når Banedanmark næste år starter udskiftningen af forældede signalsystemer med ny teknologi, vil en ny form for sikkerhedsberegning blive taget i brug. Matematiske metoder udviklet på DTU Compute gør det muligt at øge sikkerhedsniveauet på de danske jernbanestrækninger.
”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. Det skyldes, at signalsystemerne er gamle, nedslidte og baseret på en teknologi, som er ved at være forældet. Derfor starter Banedanmark nu et komplet udskiftning af samtlige signaler i hele landet. De kendte signaler med blinkende lys, som i dag står langs banen, forsvinder. I stedet flytter signalerne ind på lokoførerens computerskærm.
Tester sikkerhed
Formålet med de nye signaler er ikke blot færre forsinkelser, men også at man kan køre med flere tog og ved højere hastigheder og sidst, men ikke mindst, vil sikkerheden blive forbedret.
Og netop sikkerheden har været omdrejningspunktet for et forskerhold ved DTU Compute, der i samarbejde med bl.a. Banedanmark og Bremens Universitet har udviklet en ny matematisk metode til at teste sikkerheden af de nye systemer. Projektet er en del af et stort interdisciplinært forskningssamarbejde, finansieret af Det strategiske Forskningsråd, kaldet RobustRailS.
”Det nye signalsystem består af nogle meget komplekse softwaresystemer. Og vi har undersøgt, hvordan man med matematiske metoder kan tjekke, om systemerne rent faktisk virker som de skal. Til det formål har vi valgt at fokusere på det mest sikkerhedskritiske, nemlig de såkaldte sikringsanlæg, som skal sørge for, at der ikke sker togsammenstød og afsporinger”, fortæller lektor ved DTU Compute Anne Haxthausen.
Ingen farlige tilstande
Sikringsanlæggets opgave er bl.a. at reservere ruter til togene, styre sporskifter og give køretilladelser. Det danske fjernbanenet består af 32 sikringsanlæg, som hver styrer en bestemt del af jernbanenetværket f.eks. en meget stor station eller en strækning med flere stationer. Med det nye matematiske værktøj, udviklet på DTU Compute, kan man i en editor tegne hele det stykke jernbanenetværk som styres af et sikringsanlæg, og så generes der automatisk en matematisk model af systemet, og af de sikkerhedsegenskaber der gælder, f.eks. at to tog aldrig må være på den samme sektion samtidig. Ligesom man aldrig må ændre sporskiftets indstilling, mens toget passerer det. Et andet værktøj tjekker så, at sikkerhedsegenskaberne altid er opfyldt, uanset hvilken tilstand systemet befinder sig i.
Matematisk gennembrud
DTU forskerne har nu afprøvet metoden og skabt en model af togruten fra Roskilde over Køge til Næstved, en af de første strækninger, som får det nye signalsystem. Og udover at kunne give Banedanmark den glædelige besked, 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. Derfor har man indtil nu, kun kunne gøre dette for meget små dele af et netværk. Så snart man har forsøgt sig med længere strækninger, er computeren løbet tør for hukommelse. Men ved at bruge induktionsbeviser og noget man kalder SMT baseret, model-tjekking er det faktisk lykkedes os at modellere en 55 km lang linje med hele 8 stationer. Siden vi for nylig publicerede disse resultater, har vi oplevet en meget stor interesse, fordi resultaterne åbner nye muligheder ikke blot for test af sikkerhedskritiske systemer, men også for design og udvikling af nye systemer. En af fordelene ved at anvende metoden er nemlig, at man i princippet kan opstille en model og teste hele systemet, inden man rent faktisk udvikler softwaren”, forklarer Anne Haxthausen, og fortsætter:
”Der er heller ingen tvivl om, at matematiske metoder er fremtiden indenfor trafiksystemer. Den europæiske standard (CENELEC EN 50128) for udvikling af software til jernbaneapplikationer anbefaler stærkt, at man bruger matematiske metoder, fordi det øger sikkerheden. At formulere systemegenskaberne i en matematisk model forudsætter også 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”, slutter Anne Haxthausen begejstret.