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.