DFF-støttet ITU-projekt skal udvikle teoretisk fundament for probabilistiske sessionstyper
Stigende teknologisk kompleksitet kræver en probabilitisk tilgang til kritisk vigtige it-systemer. Et nyt forskningsprojekt, anført af lektor på ITU Marco Carbone, vil skabe fundamentet for probabilistiske sessionstyper.
Marco CarboneForskningbevillinger
Skrevet 6. marts 2025 11:47 af Theis Duelund Jensen
Distribuerede systemer bliver mere og mere komplekse, og det er afgørende at sikre stabilitet, især når det handler om fx medicinsk udstyr. Systemer udviser ofte uforudsigelig adfærd, det kommer vi ikke udenom, og det er derfor er det vigtigt at forstå systemerne ved hjælp af sandsynlighedsberegning.
Her kommer et nyt projekt ledet af lektor Marco Carbone ind i billedet. PROBABILIstic Session Types (PROBABILIST), der nyligt er blevet tildelt ca. 3 millioner kroner fra Danmarks Frie Forskningsfond, har til formål at udvikle det teoretiske grundlag for probabilitiske sessionstyper.
Sessionstyper er protokolannoteringer, der bruges af programmører til at beskrive de protokoller, deres programmer skal følge, når de kommunikerer med andre komponenter i et distribueret system. Probabilistiske sessionstyper muliggør beskrivelse af protokoller med indbygget usikkerhed. Projektetet er grundlaget for udviklingen af værktøjer til at arbejde med specifikationer af probabilitiske sessionstyper. Tilgængeligheden af den slags værktøjer vil i fremtiden få stor betydning for distribuerede systemer, især systemer, der gør brug af sandsynlighedsberegninger, herunder generel kunstig intelligens.
"Målet med projektet er i sidste ende at udvikle grundlæggende teknikker til at ræsonnere om distribueret software med et stærkt fokus på statistisk ræsonnement," siger Marco Carbone.
Som eksempel bruger forskeren en telefonapp, en sensor til måling af blodsukker og en insulininjektor, der koordinerer en patients daglige behandlinger ved at udveksle beskeder med hinanden:
"Hvis så meget som en enkelt besked lander et forkert sted, kan det sætte en diabetikers liv i fare. Desværre afhænger korrekthed i et sådant system ikke kun af de tre nævnte komponenters kode, men også af eksterne begivenheder, der ikke er præcist forudsigelige, hvilket tvinger systemet til at træffe beslutninger baseret på statistiske antagelser."
Telefonen i eksemplet kan støde på et hardwareproblem, eller endnu værre, sensoren kan udføre en fejlagtig måling. Hvis uheldet er ude, vil appen så være i stand til at opdage og korrigere fejlagtige data? Og hvordan vil det påvirke de efterfølgende beslutninger, der tages af systemet baseret på denne fejlagtige input?
"Selvfølgelig kræver ræsonnementet om korrektheden af den type systemer en tilgang, der inddrager statistisk ræsonnement: vi kan ikke længere kategorisk udelukke, at fejl vil ske. Vi må i stedet tale om, hvad sandsynligheden er for, at der sker noget utilsigtet?" siger Marco Carbone.
Derfor er behovet for at sikre korrekthed og driftssikkerhed af systemerne afgørende, hvilket kræver en dybere forståelse af de grundlæggende principper for, hvordan systemerne opfører sig, herunder hvordan de forskellige komponenter interagerer.
PROBABILIstic Session Types (PROBABILIST) finansieres af Det Frie Forskningsråd og vil løbe over en periode på tre år. Projektet er et samarbejde mellem IT-Universitetet i København, University of Oxford og Gran Sasso Science Institute.
Theis Duelund Jensen, Presseansvarlig, telefon +45 2555 0447, email