Automated Deductive Verification of Safety-Critical Embedded Software
Tid: Fr 2024-03-15 kl 13.00
Plats: Kollegiesalen, Brinellvägen 8, Stockholm
Videolänk: https://kth-se.zoom.us/j/61999411575
Språk: Svenska
Ämnesområde: Datalogi
Respondent: Christian Lidström , Teoretisk datalogi, TCS
Opponent: Professor Bernhard Beckert, Karlsruhe Institute of Technology, Karlsruhe, Germany
Handledare: Dilian Gurov, Teoretisk datalogi, TCS; Musard Balliu, Teoretisk datalogi, TCS
QC 20240223
Abstract
Inbyggda system finns överallt i samhället, och i många industrier, exempelvis fordonsindustrin, är inbyggda system säkerhetskritiska. Inbyggda system är idag också alltmer säkerhetskritiska, med framsteg inom till exempel autonoma fordon. På grund av detta finns det ett behov av metoder som kan tillse korrekthet av sådan mjukvara, och av processer och ramverk för att tackla den ökande storleken och komplexiteten hos mjukvaran. Konktraktbaserad design är en väletablerad metodologi inom design av inbyggda system, där komplexiteten i inbyggda system hanteras genom användande av konktrakt för att dela upp ansvar bland de olika komponenterna i systemet.
Denna avhandling presenterar ett formellt kontraktsramverk, eller teori, som följer principerna inom kontraktbaserad design. Teoring är utvecklad för mjukvara med funktioner, och endast definierad semantiskt, vilket tillåter den att instantieras med olika språk för att definiera kontrakt och komponenter, beroende på vad som är lämplig för olika användningsområden. Teorin är parametrisk i den semantiska domänen, vilket möjliggör att olika typer av beteende kan resoneras kring. Avhandlingen presenterar också olika instantieringar av teorin, vilket visar hur både lågnivåegenskaper kan specificeras med Hoarelogik eller ACSL, samt temporala högnivåegenskaper med temporala logiker som exempelvis TLA+. Teoring tillåter också att olika semantiska domäner kombineras. Inom teorin kan lågnivåkomponenter verifieras gentemot deras kontrakt på ett sådant sätt att de mer abstrakta högnivåegenskaperna kan visas vara uppfyllda när komponeterna sätts samman.
En vanlig metod för att verifiera korrekhet hos lågnivåmjukvara är deduktiv verifikation, och Frama-C är ett välkänt verktyg i vilket mjukvara skriven i C kan deduktivt verifieras. Avhandlingen presenterar också arbete inom kontraktgenerering, i form av ett verktyg i vilket funktionskontrakt kan genereras och användas för verifiering. Metoden bygger på TriCera, en modellprovare för C-program, och genererar kontrakt som kan anvädnas i Frama-C. Slutligen presenterar avhandlingen också ett ramverk för programinstrumentation, för att förenkla verifiering av vissa egenskaper. I detta ramverk omvandlas program med specfikationer innehållandes egenskaper som vanligtvis är svåra att verifiera till program med specifikationer utan dessa egenskaper, på ett sätt som säkerställer att om det nya programmet är korrekt, så är också originalprogrammet korrekt. Avhandlingen presenterar konkreta instrumentation för så kallade utökade kvantifikatorer, vilka är en typ av aggregering över fält, till exempel summan av alla värden, eller det maximala värdet, i ett fält.