Når et Airbus-fly letter, sker det ved hjælp af mange forskellige sikkerhedskritiske softwareprogrammer, der kan have stor betydning for flysikkerheden under take-off, flyvning og landing.
Før et softwareprogram godkendes til brug i flyet, skal det igennem en omfattende certificering, hvor det tjekkes, om softwaren overholder den internationale flyindustris softwarestandard DO-178B.
Kode uden pointere
Tilsvarende standarder findes også indenfor softwaresystemer til tog og jernbaner samt til generelt sikkerhedskritiske systemer.
Standarderne giver retningslinier for, hvordan koden skal udvikles, for at koden kan blive godkendt til fly- og jernbanebrug.
Generelt må der eksempelvis ikke anvendes dynamisk memory-allokering, da det giver mulighed for memoryleaks og softwarefejl.
Det kan være en særdeles kompliceret og dyr proces at få certificeret kode, hvorfor der ofte anvendes certificerede værktøjer som Wind Rivers VxWorks DO-178B Platform eller Esterel Technologies SCADE Suite.
SCADE Suiten genererer automatisk kode, der overholder standarderne, som er specificeret for flyindustrien i DO-178B, for jernbanen i EN 50128 og industrien i IEC 61508.
Da værktøjerne er certificeret til at overholde DO-178B, EN 50128 og IEC 61508, opfylder den genererede kode de gældende standarder.
Programmørerne skal ikke kode
For at få koden genereret kræver det, at kravene specificeres på en klar og entydig måde.
"Kravene skal formuleres helt entydigt, ikke verbalt, da der skal være et 1-1 forhold mellem specifikation og kode.
Typisk sker det ved hjælp af tilstandsmaskiner for jernbanesystemer," forklarer civilingeniør Jørleif Joensen, som gennem mange år har arbejdet med sikkerhedskritiske tekniske it-systemer hos virksomheder som den københavnske Metro, DSB, Danfoss og Vestas gennem sit selskab Joensen Consult, der også er distributør af Esterel Technologies SCADE-værktøj.
Ved at lade værktøjet generere koden, fjerner man risikoen for, at en programmør laver fejl.
""Programmøren tages ud af loopet, fordi han kan lave fejl," siger Jørleif Joensen.
Matematisk tjek af model
Det er ikke kun kodegenereringen, der er med til at fjerne fejlkilder. Værktøjet kan tjekke, om modellen for systemet er korrekt.
"Esterels værktøjer arbejder med matematiske metoder, som modvirker, at der introduceres fejl. Der kan eksempelvis være et sikkerhedskrav om, at landingshjul kun kan udløses, når flyet når under en bestemt hastighed, da det ellers vil blive revet af. Der defineres så en safety-property for softwaren: Hvis hastighed er større end x, så sænkes landingshjul ikke. Værktøjet tjekker, at den safety-property aldrig overskrides," forklarer Jørleif Joensen.
Man kan ikke teste sig til sikre systemer
Det er en bedre måde at udvikle software på end en mere test-baseret udvikling. Ifølge Jørleif Joensen kan man nemlig ikke teste sig til sikre systemer
"Test kan aldrig afskaffes, men test er absolut ikke nok. Man kan ikke teste sig til sikker software. Hele modellen med test, inspektion og kodereview virker ikke godt nok. Den giver større sandsynlighed for, at der ikke er farlige fejl, men man kan ikke sige noget konkret om, hvor sikker softwaren er," mener Jørleif Joensen.
Fejl kan opstå i specifikationen
Selvom modelverifikation og modelbaseret kodegenerering giver mere sikker software, understreger Jørleif Joensen, at modelverifikation og kontrolleret kodegenerering i sig selv ikke udelukker fejl.
"Det er ikke fool-proof. Tog- og fly-software bør være 100 procent sikker. Det er der ikke er noget, der er, men der er stort fokus på det. Der kan være logiske fejl i specifikationen, som man ikke kan sikre sig imod. Det kunne eksempelvis være, at man har angivet en forkert safety property som hastigheden, hvor landingshjulet kan udløses," siger Jørleif Joensen.
Ikke nok fokus, men det kommer
Ifølge Jørleif Joensen er modelverifikation begyndt at få vind i sejlene.
"Der er for få mennesker, der interesserer sig for det her, men industrien får flere krav og modelbaseret software med matematiske verifikationsværktøjer begynder at vinde indpas. Jeg forventer, at forretningsområdet vil eksplodere," siger Jørleif Joensen.
Det er altovervejende indenfor teknisk software at modelverifikation vinder indpas.
"Det er til teknisk software, da kodegenereringen giver begrænsninger. I sikkerhedskritiske, tekniske indlejrede systemer er man ikke så meget for pointere, da der notorisk sker fejl med pointere. Så den genererede C-kode er uden de mere frække ting. Men det kan da godt være, at ERP og administrative systemer på sigt kommer med," siger Jørleif Joensen.
