22. mars: Hvordan utvikle korrekte datasystemer?

Kort om foredraget:

Vi befinner oss i den litt paradoksale situasjonen at våre liv og vår velferd stadig blir mer og mer avhengig av at datasystemer funker som de skal, samtidig som disse datasystemene blir stadig større og mer kompliserte, og derfor nesten umulig å få feilfrie.

Det er tilstrekkelig å nevne nettbanker og handel med kredittkort, biler (som i stor grad styres av et nettverk av små datamaskiner), fly, e-regjering (selvangivelse, etc.), og ulike former for datasystemer i helsevesenet, og så videre. Disse systemene er typisk distribuerte systemer som består av mange "datamaskiner" koblet sammen i et (ofte "ad hoc") nettverk. Det er velkjent at det er meget vanskelig å designe korrekte distribuerte systemer.

Formell modellering og analyse er en måte å prøve å utvikle så korrekte datasystemer som mulig. Poenget er at man lager en modell av designen av det ønskede datasystemet, akkurat som en arkitekt lager tegninger og modeller av et hus før man setter igang byggingen av huset.

En høynivå modell av et datasystem (dvs., en modell som ser bort fra "implementasjonsdetaljer" og fokuserer på designen/ideen/algoritmen i systemet) er vel og bra, og kan sikkert brukes til noe, men ideelt sett ønsker man ikke å bare se på en modell, men å la en datamaskin analysere modellen på ulike måter. I formell modellering lager man en matematisk modell av systemets design, og man kan da la datamaskinen foreta ulike former for matematisk analyse av modellen før den implementeres. For eksempel kan man la datamaskinen systematisk lete etter mulige feilsituasjoner, eller man kan bruke datamaskinen til å bevise at designen tilfredsstiller visse ønskede egenskaper.

Forelesningen vil være en lettforståelig motivering og innføring i slik formell modellering og analyse av mer eller mindre korrekthetskritiske datasystemer.

Oppsummering skrevet av Ragnhild Kobro Runde:

Samfunnet er avhengig av korrekte og pålitelige datasystemer, samtidig blir disse stadig større og mer kompliserte. Eksempler på systemer hvor det er kritisk hvis ting går galt inkluderer fly, banksystemer, krigføring styrt via satellitter og vanlige biler hvor små datamaskiner erstatter mer og mer av mekanikken.

Datasikkerhet

Bruk av nettbank er et eksempel hvor datasikkerhet er viktig. På nettet er det lett både å avlytte kommunikasjon og å sende falske meldinger. Så hvordan kan nettbanken vite at den kommuniserer med den faktiske eieren av kontoen, og hvordan kan brukerne vite at han kommuniserer med den ekte banken? NSPK er en protokoll for slik gjensidig autentisering. NSPK ble mye brukt fra 1978, men ble formell analyse viste i 1995 at den ikke er sikker likevel. Det tok altså 17 år å finne feilen - på tross av at protokollen essensielt bare består av tre linjer "kode"!

Spørsmålet blir da hvordan man kan sikre at viktige systemer korrekt. Her finnes det mange teknikker som utfyller hverandre, og formell modellering og analyse av systemdesign er en viktig del av dette.

Modellering

Modellering vil si å lage en plan/beskrivelse av hvordan systemet er tenkt å fungere - tilsvarende hvordan arkitekter lager ulike typer modeller av bygningene før selve byggingen starter. Sammenlignet med å lage et ferdig datasystem, går det raskt å lage en modell av systemet som inkluderer de viktige delene av systemet, med hvor detaljer som ikke har noe med designideene å gjøre er abstrahert bort. Modellen kan så brukes til å analysere designet med tanke på spørsmål som: Kan flyet styrte? Er det mulig å lure nettbanken? Vil airbagen utløses raskt nok ved en kollisjon? Dersom analysen viser at designet er tilfredsstillende, fungerer modellen som et fundament for implementasjon av systemet.

Formelle modeller og analysemetoder

En formell modell er basert på matematisk logikk, og modellen er et matematisk objekt. Det vil si at modellen er entydig, at matematiske regler kan brukes til å analysere konsekvenser av designen og at klare slutningsregler gjør at analysen i stor grad kan automatiseres.

I foredraget skilte Peter mellom tre hovedtyper av analysemetoder:

• Simulering, hvor man eksekverer en mulig oppførsel av systemet. Dette gir god informasjon om denne ene oppførselen, men fungerer dårlig hvis systemet har mange mulige oppførsler (også for samme input), noe som stort sett er tilfellet når det er snakk om nettverk.
• Modellsjekking, hvor man automatisk analyserer alle mulige oppførsler ut fra en start-tilstand. Dette fungerer bra ikke minst for å finne mer uvanlige feil, men det kan være et problem hvis det blir altfor mange mulige oppførsler (tilstander).
• Bevise teoremer, hvor man fører et matematisk bevis for at visse egenskaper holder. Dette er ikke-trivielt, og selv om deler kan automatiseres krever det ofte også mye menneskelig hjelp.

Formelle metoder på ifi

For å få systemdesignere til å benytte formelle metoder, er det viktig med enkle og intuitive formalismer og analysemetoder. En mulighet er å definere en formell semantikk til et intuitivt modelleringsspråk som allerede brukes av systemdesignere - for så å automatisk oversette den uformelle modellen til en formell modell for videre analyse. PMA-gruppen ved ifi bygger sin virksomhet på omskrivingslogikk og Maude - et formelt språk og verktøy for simulering og modellsjekking, med mange likhetstrekk med funksjonell programmering. Spesielt har PMA-gruppen utviklet Real-Time Maude, en utvidelse av Maude for å kunne modellere og analysere systemer hvor sanntid spiller en avgjørende rolle. Basert på Maude har PMA-gruppen også utviklet språket CREOL, som blant annet har vært brukt til å verifisere en modell av en mengde autonome støvsugere.