Lars Birkedal har netop modtaget bevillingen fra Det Frie Forskningsråds forskerkarriereprogram Sapere Aude: DFF-Topforsker.

Populært sagt rammer Lars Birkedals forskning noget, vi alle har stiftet bekendtskab med: Software med fejl. Han forsker i, hvordan man kan undgå fejlene og finde dem, før vi oplever vores program lukker ned.

Det er der stor interesse for og med bevillingen fra Det Frie Forskningsråd kan vi nu komme nærmere løsningerne.

- Softwarefejl er irriterende for den enkelte forbruger, men det er kritisk for et moderne samfunds infrastruktur. Vigtigheden er på linje med rent vand. Fejl eller sikkerhedsbrist er blandt de største udfordringer i softwaresystemer.

Fejl åbner mulighed for eksempelvis hackerangreb, der kan sætte hele verden i stå. Med vores værktøjer vil softwarefejl i fremtiden kunne opdages inden de viser sig. Det er det midlerne skal gå til, forklarer Lars Birkedal.

Han står i spidsen for den nyopstartede forskergruppe inden for logik og semantik på datalogi i Aarhus. Midlerne giver plads til nye post.doc og ph.d.-stillinger, der skal videreudvikle de nuværende matematiske modeller og logikker til at beskrive og analysere software for i sidste ende at kunne forbedre den.

- Vort arbejde vil danne grundlag for udviklingen af praktiske softwareværktøjer, som kan assistere programmører med at udvikle korrekt software, siger han.

Tænk dig til alverdens fejl

Ifølge Lars Birkedal handler deres forskningsområde grundlæggende om, at det er svært at lave software, der fungerer efter hensigten. Software er bygget op af komplicerede systemer, og vi bruger dem overalt. Til at styre fly, biler eller finansielle transaktioner. Det skal fungere korrekt altid, men det er komplekst og svært at sikre sig, at der ikke er fejl.

- Man undervurderer, hvor svært det er at lave software. Man skal både vide, hvad programmet skal på det tekniske niveau og samtidig sikre sig det kører effektivt og uden fejl. Samtidig er software blevet meget mere komplekst. Det har man talt om i teorien, og nu oplever man det i praksis. Man skal tage højde for mange tænkelige og utænkelige situationer, siger han.

Det klassiske eksempel er raketten, der springer i luften kort efter afsendelse eller bilproducenter, der må tilbagekalde biler pga software fejl. Og fejl man gerne ville have fundet, inden de opstod.

- Derfor er der stor interesse for vores forskning. En måde at hjælpe til at undgå fejl er bedre værktøjer til at analysere programmer og hvordan de virker. For at kunne det er det nødvendigt med detaljerede matematiske modeller, forklarer han.

Værktøjer til udviklere

Lars Birkedal bruger sin viden til at udvikle teknikker til værktøjer, der i sidste ende skal bruges af udviklere. Værktøjer kan i dag finde fejl, men man vil gerne udvide den klasse af fejl, som værktøjer kan afhjælpe. Midlerne skal bruges til at skrive bedre formler og specifikationer, som tjekker om de forskellige antagelser og forventninger er opfyldt.  Jo mere detaljeret jo mere komplekst bliver det.

- Pointen er at nogle af de problemer som eksempelvis sikkerhedsbrister skyldes detaljerede tekniske fejl. Vi prøver at analysere programmer, der kører, og de modeller vi laver skal tale med de programmer, der kører og støtte de udviklere der laver dem. Hvis modellerne er for abstrakte kan man ikke opdage problemerne, understreger Lars Birkedal.

Mere teknisk detaljeniveau

Det overordnede mål om bedre modeller  har været kendt i mange år, men man har ikke haft teknikkerne til at adressere udfordringerne tilstrækkeligt. Men der er sket en række fremskridt de sidste 10 år,  som Lars Birkedel vil bygge videre på i projektet. Specielt ser Lars Birkedal på programmeringssprogs features som er særligt udforende at lave modeller for.

- Moderne programmeringssprog kombinerer programmeringssprogselementer, såsom delte opdaterbare datastrukturer, objekter, højere-ordens funktioner, og parallelitet, som er særligt udfordrende. De seneste år er der sket en række fremskridt i bevisværktøjer samt modeller og programlogikker for sprog, der kombinerer delte opdaterbare datastrukturer med objekter og højere-ordens funktioner, samt en række fremskridt for lavniveau sprog med parallelitet. I projektet vil vi udvikle nye modeller og programlogikker for sprog, der kombinerer alle disse udfordrende features, siger han.

- Vi udvikler nogle nye programlogikker og type systemer, som gør det muligt at give en præcis matematisk beskrivelse af hvad et program skal gøre. Vi fokuserer specielt på at udvikle modulære modeller, således at det er muligt at beskrive og analysere hvert programmodul for sig. På den måde vil vore teknikker forhåbentlig kunne skalere til store systemer, forklarer han.

- Objekter og højere-ordens funktioner er vigtige for programmører fordi de gør det muligt at opsplitte et program i en række programmoduler som kan forstås hver for sig og som kan udvikles af forskellige programmører. Det er også vigtigt af hensyn til at kunne lave programbiblioteker. En af udfordringer i projektet er at sikre at de nye matematiske modeller bliver tilsvarende modulære.

- Delte opdaterbare datastrukturer er vigtige i programmering for at kunne implementerer effektive algoritmer. Men det er udfordrende at beskrive og analysere programmer, der benytter delte opdaterbare datastrukturer. Intuitivt fordi man skal passe på, at et modul ikke ændrer i en datastruktur uden at et andet opdager det.

- Moderne computere udfører beregninger i parallel, på flere processorer på samme tid. Dermed kan flere processorer opdatere datastrukturer på samme tid, med uforudsete resultater til følge. Det kan man løse ved at låse datastrukturerne, men så er problemet, at du ikke udnytter paralleliteten optimalt,  og dermed ikke får den ønskede effektivitet. Vore nye modeller vil også kunne bruges til at beskrive og analysere avancerede parallelle programmer, der ikke bruger låse.

Færre softwarefejl

Det er vigtigt for producenter af software, at de bliver kendt for få softwarefejl. Løbende opdateringer af software sker eksempelvis, fordi producenten har fundet fejl af forskellig art.

Microsoft investerer i at prøve at lave bedre værktøjer i deres egne forskningsafdelinger i samarbejde med Lars Birkedal. På den måde finder Lars Birkedals forskning anvendelse i industrien.

- De bruger vores forskning til at udvikle værktøjer som deres forskere tager videre til produktgrupperne. Desuden er der lavet start-up virksomheder, der udvikler analyseværktøjer og finder fejl i samarbejde med producenter  og industri, siger han.

Kontakt:

Lars Birkedal, Institut for Datalogi, Aarhus Universitet, tlf. 2383 8546