Dansk forskningsprojekt skal forbedre fejlfinding i distribueret software

Lektor ved IT-Universitetet Marco Carbone. Illustration: IT-Universitetet
Endnu et dansk projekt arbejder med beviselighed i software.

Et nyt forskningsprojekt på IT-Universitetet skal udvikle matematiske modeller, der kan være med til at forbedre fejlfinding i programmer.

Projektet, der hedder 'Mechanisation of Session Types', har som sit primære fokus på distribueret software – programmer, der kører sideløbende på flere enheder og maskiner – og den interne kommunikationsproces mellem softwarens forskellige dele.

Ifølge lektor ved IT-Universitetet Marco Carbone, som leder projektet, er der behov for at forbedre den metodiske tilgang til problemet. Hans projekt ser på, hvordan softwaredele interagerer med hinanden via såkaldte session types, en teoretisk måde at kategorisere kommunikation i software på.

Ved at benytte sig af en såkaldt bevisassistent, der automatiserer evalueringen af session type-parametre ved hjælp af matematiske beviser, håber Marco Carbone på at sikre bedre fejlfinding i fremtiden.

Maskinevaluerede beviser

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.

»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,« udtaler Marco Carbone i en meddelelse.

Projektet er ikke det eneste i Danmark, der prøver at løse problemet med beviselige programmer. På Aarhus Universitets Center for Grundforskning i Program-verifikation er målet at udvikle bedre teknikker til at sikre softwaresystemer. Her forskes der også i udvikling af metoder og værktøjer, der kan bevise, at et givent program ikke indeholder fejl.

Læs også: Dansk center vil skabe værktøjer til fejlfri programmering

»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,« siger Marco Carbone fra IT-Universitetet.

»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.«

En bevilling fra Danmarks Frie Forskningsfond skal bruges til at ansætte en ph.d.-studerende på projektet, som kan videreudvikle Marco Carbones teorier.

Tips og korrekturforslag til denne historie sendes til tip@version2.dk
Følg forløbet
Kommentarer (0)
sortSortér kommentarer
  • Ældste først
  • Nyeste først
  • Bedste først
Log ind eller Opret konto for at kommentere