Matematik mindsker risiko for togkollison

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

”Udskiftningen af samtlige signaler er en kæmpe investering, som vil forbedre togdriften i Danmark markant,” fortæller Henrik Holtermann, sekretariatschef i Banedanmarks signalprogram, og fortsætter: ”Når de mange fejl, der skyldes systemernes alder og gammeldags teknik, fjernes, får vi en langt mere stabil jernbanedrift i hele landet. Derudover vil regulariteten blive forbedret, så passagererne vil opleve, at flere tog kommer til tiden. Takket være de nye, avancerede softwaresystemer, som fremover styrer signalerne, bliver der også bedre kapacitet nogle steder i jernbanenettet. Den kan vi anvende til flere tog eller højere hastigheder på visse strækninger. Og sidst, men ikke mindst, vil vi opnå samme høje sikkerhedsniveau på alle strækninger i landet.”

Tjekker sikkerheden

Og netop sikkerheden har været omdrejningspunktet for et forskerhold ved DTU Compute, der i samarbejde med Banedanmark 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.

Forskerne på DTU har udviklet en helt ny matematisk metode under beregningen af signalsystemernes sikkerhed.  Det nye værktøj genererer automatisk en matematiske model af systemet og checker, at dets sikkerhedsegenskaber er opfyldt.

Grafik DTU Compute

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 kan man i en editor tegne det stykke jernbanenetværk, som styres af et sikringsanlæg. Herefter genereres 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.

Forskernes skematiske fremstilling af jernbanesikkerhedsrisici som f.eks. kollision, frontal kollision og togafsporing.

Grafik DTU Compute

Bevisbyrden bliver lettere

Hos Trafik- og Byggestyrelsen hilser man den nye metode velkommen. ”Udfordringen ved disse sikkerhedskritiske systemer er, at de altid skal tilpasses den eksisterende struktur i det lokale jernbanenetværk. Og som det er i dag, er softwareændringer lig med en meget tidskrævende og omstændelig proces, fordi leverandøren efterfølgende skal bevise, at systemerne stadig er sikre. Vi er derfor meget tilfredse med, at der nu er udviklet nogle formelle metoder, som gør det nemmere at bevise, at sikkerheden er i orden. Vi ser meget gerne endnu mere forskning i nye metoder til at effektivisere fejlretning, verifikation og godkendelsesprocesser, da kompleksiteten i disse systemer gør, at det er meget tungt for virksomhederne,” forklarer Jesper Rasmussen, vicedirektør i Trafik- og Byggestyrelsen.

Figuren er et eksempel på, hvordan forskerne arbejder med bevisopgaven: Den viser de potentielle systemtilstande, hvoraf nogle er sikre, andre usikre (de hvide og sorte prikker). Og den viser mulige tilstandsændringer (pilene). Kun nogle af tilstandene er mulige, dvs. at de kan nås fra starttilstanden tv. Bevisopgaven er at vise, at alle de mulige tilstande er sikre. Og det er tilfældet i dette eksempel.

Grafik DTU Compute

Matematisk gennembrud

Når Banedanmark starter udrulningen af de nye signalsystemer i 2016, bliver togruten fra Roskilde over Køge til Næstved en af de første strækninger. Derfor var det netop sikringsanlægget for denne rute, som DTU-forskerne byggede en matematisk model af for at afprøve sikkerheden af signalsystemet med deres nye metode. Og ud over 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 kunnet 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 vi har nu udviklet en ny og smartere metode, som har gjort det muligt at verificere en model af den 55 km lange linje fra Roskilde til Næstved med hele otte stationer. Kernen i vores metoder er, at vi bruger en ’model checker’ 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. Idéen i induktionsbeviset er, at man først beviser, at start-tilstanden er sikker. Derefter beviser man et såkaldt induktionstrin. I dette trin skal man vise, at for enhver tilstand, der er sikker, er dens næste tilstand også sikker. Hvis dette trin også er ok, kan man slutte, at alle tilstande, der kan nås fra starttilstanden, er sikre. (Se figuren ovenfor). Når man bruger denne metode, anvender man et værktøj kaldet RT-tester til automatisk at udføre induktionsbeviserne. Værktøjet er udviklet ved Universität Bremen, men har ikke tidligere været anvendt til at foretage induktionsbeviser. Og tilsammen er det blevet til 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 at tjekke 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 bevise sikkerheden af hele systemet, inden man rent faktisk udvikler softwaren. Det vil på sigt kunne spare virksomhederne for tid og penge i softwareudviklingen, for jo senere i udviklingsprocessen, man opdager fejl, jo dyrere er det at rette,” forklarer Anne Haxthausen og fortsætter:

”Der er heller ingen tvivl om, at matematiske metoder er fremtiden inden for trafiksystemer. Den europæiske standard (CENELEC EN 50128, red.) 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, 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.