Er ESARR 6 nok ?

Jeg rendte ind i en hyggelig fætter fra Luftfartstilsynet forleden dag og når han engang er færdig med at godkende mit nuværende håndarbejde skal jeg have en sludder med ham om "ESARR 6".

I har med garanti aldrig hørt om ESARR 6, men jeg synes i skal læse den, det er kun 16 sider og det meste er fyldstof.

Den officielle titel er "Software in Air Traffic Management Systems" og de 16 sider er principielt det eneste der står imellem en blue-screen-of-death og jeres fly når det lander.

Arbejdsgrupper under EuroControl arbejder på at få udgivet den nødvendige "guidance".

Den eneste omtale af kildetekst er på side 37 i guidance dokumentet, i diskussionen om COTS (Comercial Off the Shelf) software:

In particular, the commercial sensitivity of these systems makes it unlikely that ANSPs will obtain the source code that can be necessary to perform 'white box' tests that deliberately expose potential weaknesses using a knowledge of the internal implementation.

For nu at stoppe alle autoaversioner med det samme, så er det ikke kun Microsoft de hentyder til. Dokumentet fortsætter:

It is, therefore, more difficult to convince designated authorities that the requisite level of rigour has been used to support the development and deployment of COTS for higher software assurance levels.

Det er svært ikke at have den sætning rungende i hovedet, når man sidder et par kilometer oppe og ser Københavns tårne nærme sig.

Ude i Kastrup har Naviair brugt en rund milliard fra finansloven på at modernisere de danske ATM systemer og jeg har fornøjelsen af at være underleverandør til projektet, der har cut-over d. 28 december i år.

Det siger sig selv at Naviair får leveret både kildetekst og CVS træet med til den software jeg skriver for dem.

Og jeg har heller ingen fingre at sætte på hverken Naviair eller deres underleverandører, alle jeg har mødt har en forståelig ærbødighed overfor opgaven og en meget professionel indstilling til at gøre tingene ordentligt.

Men burde der trods alt ikke have stået noget mere om kildetekst og været et krav om code review i ESARR6 ?

phk

Kommentarer (7)
sortSortér kommentarer
  • Ældste først
  • Nyeste først
  • Bedste først
Torben Mogensen Blogger

Jeg skimmede lige ESARR6 dokumentet, og det bruger en del tekst på "software verification assurances". Det vil vel indebære code review, med mindre man decideret bruger automatiske formelle verifikationsværktøjer.

Men du har ret i, at man godt kunne tænke sig nogle garantier omkring koden og specifikationen:

  1. At specifikationen af softwaresystemet er tilstrækkeligt præcis til at man kan opstille en fyldestgørende samling af formelt logiske udsagn, som man kan holde op mod implementeringen og verificere denne formelt.

  2. At specifikationen udover en rent logisk funktionsbeskrivelse ogsa angiver intentionen, så man kan verificere om specifikationen opfylder intentionen.

  3. At koden er skrevet i et sprog, der har en entydig semantik, gerne formelt beskrevet.

  4. At implementeringen af sproget er valideret til at være konsistent med semantikken, enten ved omfattende test eller ved formel verifikation.

  5. At hardwaren er verificeret til korrekt at implementere den eksekveringssemantik, som dokumentationen foreskriver.

Men det er måske for meget forlangt?

  • 0
  • 0
Poul-Henning Kamp Blogger

Torben,

Jeg er forholdsvis pragmatisk indstillet, jeg tror ikke vi nogensinde når til systemer der er bevist formelt korrekte der samtidig er komplekse nok til at løse relevante opgaver.

Så ja, din drømmeliste er meget morsom, men ESARR6 ville ikke gøre nogen gavn hvis din liste var indbeffattet, for så ville alle systemer bare få dispensation fra ESARR6 kravene.

Jeg ville være tilfreds hvis ESARR6 indeholdt blot lidt tekst jeg kunne genkende fra de sidste 50 års arbejde med at forbedre softwarekvalitet.

Poul-Henning

  • 0
  • 0
Karsten Nyblad

Tja,

Jeg læste en gang en artikel, hvor nogen havde sammenlignet stabiliteten af lukket kode med åben, og det eneste sted, hvor den lukkede vandt, var netop i sikkerhedsrelaterede anvendelser. De firmaer der leverer den slags systemer, tester deres ting, tester dem igen og så en gang til. Den mindste ændring og så starter testing igen. Den københavnske Metro og DSBs IC4 tog begge begge forsinket på den konto. Derudover skal koden være veldokumenteret, osv. En af Metroens stationer hedder Universitet, med det ligger ikke der. Problemet er bare, at det ville koste Metroen 10 millioner at rette navnet, og et af problemerne er at softwaren så skal testes igen.

Kravne er nu også ekstremt høje. Man regner med, at hvert system i et fly i snit skal virke i 10^9 flyve timer per fly der falder ned. Det er 114.000 år.

  • 0
  • 0
Torben Mogensen Blogger

Luftfartsindustrien bruger skam formel verifikation til software. Der er dog ikke tale om komplette korrektshedsbeviser, men analyser af hvorvidt bestemte fejlsituationer er beviseligt umulige.

Men du har ret i, at min liste er urealistisk på nuværende tidspunkt. Det kan dog ændre sig. Der eksisterer brugbare programmeringssprog, der er eksakt beskrevet med en formel semantik, så det er muligt at bruge denne semantik til at analysere programmers opførsel. Der findes også formelt verificerede oversættere (mestendels for små sprog, men se f.eks. http://pauillac.inria.fr/~xleroy/publi/cfront.pdf og http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf).

Som sidstnevnte artikel påpeger, så vil man lave verifikationen mens man udvikler softwaren og skrive softwaren med henblik på samme, da det er urealistisk at verificere store programmer, der ikke er skrevet med en passende disciplin.

Det svarer lidt til at skrive programmer i et statisk typet sprog. Hvis man ikke tyechecker sit program undervejs, så er det urealistisk at forvente, at typechecket kan gennemføres bagefter uden større omskrivninger. Enhver, der har prøvet at porte et Javascriptprogram til Java vil sikkert kunne genkende problemet. Tilsvarende vil man verificere hele tiden under programudviklingen. i stedet for at lave en monolitisk verifikation til sidst.

Den største hindring for verifikation af software er økonomi: Det koster en del at verificere sine programmer, så det er kun, hvis der er store beløb på spil ved fejl, at man gør det. Men det er der jo for ATM systemer.

  • 0
  • 0
Jens Fallesen

Nu hedder stationen jo rent faktisk ikke længere Universitetet andet end måske i diverse intern dokumentation, lige som stationsforkortelsen vist ikke er ændret.

Men så vidt jeg er orienteret, er det altså ikke rigtigt, at det koster nye systemtest af ændre et stationsnavn.

Normalt er den slags systemer opbygget på en sådan måde, at alle stationer er kendt under en intern kode, og så er det fuldkommen lige meget, hvad denne station præsenteres som i højttalere, på informationsdisplays og i trykt materiale.

Jeg har ikke kendskab til, at det skulle forholde sig anderledes med Metroen.

Dermed ikke sagt, at der ikke er meget store dokumentations- og testkrav til sikkerhedssystemer inden for jernbanen, for det er der i høj grad.

  • 0
  • 0
Log ind eller Opret konto for at kommentere