Nyt forskningsprojekt skal forbedre fejlfinding i software

I dag er software en essentiel del af samfundets kritiske funktioner, fra sundheds- og transportsektoren til kommunikation og energiforsyning. Et nyt forskningsprojekt, anført af lektor ved IT-Universitetet Marco Carbone, skal udvikle matematiske modeller til forebyggelse af fejl i software. Danmarks Frie Forskningsfond har netop bevilget projektet 2,8 millioner kroner.

Marco Carbone Forskning Institut for Datalogi bevillinger programmeringssprog software

Skrevet 18. maj 2021 09:58 af Theis Duelund Jensen

Samfundet er dybt afhængig af den software, der understøtter kritiske funktioner, så det er afgørende at udvikle metoder til at sikre, at softwaren fungerer, som den skal. Lektor ved ITU Marco Carbone, har netop modtaget en bevilling på 2,8 millioner kroner fra Danmarks Frie Forskningsfond til det formål.

Med forskningsprojektet “MECHANIsation of Session Types” vil Marco Carbone udvikle matematiske modeller, der så at sige gengiver softwarens DNA i et matematisk sprog, som kan være med til at forbedre fejlfinding i programmer. Projektet har som sit primære fokus på såkaldt distribueret software – programmer, der kører sideløbende på flere enheder og maskiner – og den interne kommunikationsproces mellem softwarens forskellige dele.

- En matematisk repræsentation af et stykke software kan sammenlignes med en bygningsingeniørs opstalt. Man begynder altid med en model af bygningen, eller i dette tilfælde programmet, for at sikre sig, at den ikke senere hen kollapser, siger Marco Carbone.

For mange menneskelige fejl

Og der er stort behov for bedre fejlfindingsmetoder i softwareudviklingen. Tidligere var det kun muligt at afprøve software for fejl ved hjælp af gammeldags knofedt foran tastaturet – programmøren forsøgte så godt som muligt at afprøve for alle tænkelige fejl i programmet – men der findes uendeligt mange kombinationer og ifølge Marco Carbone, er der behov for at forbedre den metodiske tilgang til problemet. Hans projekt, der er det ene af to datalogiprojekter, som Danmarks Frie Forskningsfond i år har bevilget midler til, ser på, hvordan softwaredele interagerer med hinanden via såkaldte session types, en teoretisk måde at kategorisere kommunikation i software på.

- Når man i et stykke software har flere elementer, der kommunikerer med hinanden, må man specificere, hvordan de skal kommunikere. Hvis programmet overholder session type-parametrene, kører det uden problemer. Problemet er bare, at de modeller, vi har til at evaluere den proces, kun findes i fysisk format, og de er typisk 50-100 sider lange. Hvad hvis programmøren, der skal indføre sådan en model, laver en tastefejl? Det kan sammenlignes med, at mureren, der arbejder ud fra bygningsingeniørens opstalt, lægger én mursten et sted, hvor der skal være to, siger Marco Carbone.

Ved at benytte sig af en såkaldt bevisassistent, der automatiserer evalueringen af session type-parametrene ved hjælp af matematiske beviser, håber Marco Carbone på at sikre bedre fejlfinding i fremtiden. Ideen er at gå fra matematiske beviser på papir til maskinevaluerede beviser, der på længere sigt kan bane vejen for maskinevalueret integration i eksisterende programmeringssprog til softwareudvikling. Bevillingen fra Danmarks Frie Forskningsfond skal bruges til at ansætte en ph.d.-studerende på projektet, som kan videreudvikle Marco Carbones teorier.

- På nuværende tidspunkt befinder min forskning sig på det teoretiske plan, men jeg håber på at se det implementeret i en praktisk sammenhæng i fremtiden. De fleste mennesker tænker sjældent over det, men samfundet er utroligt afhængigt af velfungerende software. Det er derfor meget vigtigt, at vi sikrer en høj kvalitet på området.