ANNONCE:
Forskning og udvikling af modelverifikation er udbredt i universitetsverdenen og SCADE-værktøjets verifikations-plugin stammer da også fra universitetsverdenen.
Pluginet til SCADE kommer fra det svenske firma Prover, der blev grundlagt af Gunnar Stålmarck, der var professor i datalogi fra Stockholm Universitet før han startede Prover.
Pluginet til SCADE kommer fra det svenske firma Prover, der blev grundlagt af Gunnar Stålmarck, der var professor i datalogi fra Stockholm Universitet før han startede Prover.
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.
Fortsættes ...



