12.1.2024
Doktorsavhandling om ramverk för kontraktbaserad design av dataflödesprogram
DI Jonatan Wiiks doktorsavhandling i datateknik framläggs till offentlig granskning vid fakulteten för naturvetenskaper och teknik vid Åbo Akademi.
Avhandlingen heter Contract-Based Design of Dataflow Programs.
Disputationen äger rum fredagen den 19 januari 2024 kl. 13 i Auditorium XXII, Agora, Vattenborgsvägen 3, Åbo, samt via videolänk. Opponent är professor Klaus Schneider, Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau, Tyskland och kustos är docent Marina Waldén, Åbo Akademi.
Sammanfattning
Det blir allt viktigare att kunna säkerställa att programvarusystem fungerar korrekt, då de i allt högre grad interagerar med vår omgivning och vi blir allt mer beroende av dessa datorsystem för att utföra vardagliga sysslor. Man kan idag hitta mycket komplicerade programvarusystem i exempelvis bilar, medicinsk utrustning och telekommunikationssystem. Fel som uppstår i den här typen av system kan ha katastrofala följder.
Avhandlingen presenterar ett ramverk för kontraktbaserad design av dataflödesprogram. Kontrakten utgör specifikationer som beskriver egenskaper som programmet bör uppfylla. Med hjälp av verifieringsmetoder som presenteras i avhandlingen kan man automatiskt bevisa att programmen uppfyller egenskaperna i kontrakten för alla tillåtna inputdata. Det påvisas också att kontrakt därutöver kan användas för att förbättra dataflödesprograms prestanda.
Dataflödesprogrammering är en programmeringsmetod där dataflödet – det vill säga kommunikationen mellan komponenter – beskrivs i form av diagram istället för vanlig programkod. Dataflödesprogram har flera gynnsamma egenskaper som förenklar utnyttjandet av moderna datorplattformars prestanda. Dessa plattformar tenderar bestå av allt fler beräkningsenheter och kan dessutom bestå av dedikerade enheter som är optimerade för att utföra vissa typer av beräkningar så effektivt som möjligt. Dataflödesprogrammering är ofta särskilt lämpligt för system som kontinuerligt interagerar med sin omgivning.
Ramverket som presenteras i avhandlingen stödjer kontraktbaserad specifikation och automatisk verifikation av flera olika typer av dataflödesprogram med funktioner och egenskaper som är vanliga i säkerhetskritiska programvarusystem. Inom ramen för avhandlingen har det också utvecklats prototypverktyg för alla föreslagna metoder. Prototypverktygen användes för att säkerställa och utvärdera metodernas praktiska användbarhet och prestanda genom att specificera och verifiera ett stort antal olika exempelprogram.
Jonatan Wiik är född 1986 i Korsholm. Han kan vid behov nås per telefon 050 371 1279 eller e-post jonatan.wiik@abo.fi.
Avhandlingen kan läsas i Åbo Akademis publikationsarkiv Doria.
Klicka här för pressbild på disputanden.
Anvisningar för att följa med disputationen på distans
För att följa med disputationen behövs programvaran Zoom eller webbläsaren Google Chrome. Du behöver inte skapa ett Zoom-konto för att kunna följa med disputationen. Om du installerar appen deltar du genom att klicka på möteslänken varefter du bör tillåta att länken öppnas i Zoom-appen.