Page 29

Dynamo_43

DYNAMO 43 12 15 DTU 29 RobustRailS Robustness in Railway OperationS er et stort tværfagligt projekt finansieret af Det Strategiske Forskningsråd. Siden 2012 har forskere fra DTU Management Engineering, DTU Transport, DTU Fotonik og DTU Compute arbejdet på at udvikle nye metoder til at sikre punktlig, pålidelig og sikker togdrift i Danmark i samarbejde med Banedanmark, DSB, DSB S-tog, Trafikstyrelsen, og Universität Bremen. 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, ”MATEMATIKKEN ER VELEGNET, DA DEN HAR EN FULDSTÆNDIG UTVETYDIG MENING.” 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. Lektor Anne Elisabeth Haxthausen, aeha@dtu.dk 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 nederst side 28). 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 ANNE HAXTHAU S E N , LEKTO R , D T U COMPUTE


Dynamo_43
To see the actual publication please follow the link above