26.8.2022

Doktorsavhandling i datavetenskap

MSc Masoumeh Parsas doktorsavhandling i datavetenskap framläggs till offentlig granskning vid fakulteten för naturvetenskaper och teknik vid Åbo Akademi.

Avhandlingen heter Diagrammatic Languages and Formal Verification: A Tool-Based Approach  

Disputationen äger rum fredagen den 2 september 2022 kl. 13 i Auditorium XX, Agora, Vattenborgsvägen 3, Åbo. Opponent är professor Philipp Rümmer, Regensburgs universitet, Tyskland och kustos är docent Marina Waldén, Åbo Akademi.  

Sammanfattning 

Vikten av en programvaras korrekthet har accentuerats då ett växande antal säkerhetskritiska system, vilka är beroende av programvaran som styr dessa, har utvecklats. En av de mer framträdande metoderna som riktar in sig på utveckling av korrekt programvara är formell verifiering. Inom formell verifiering avses med ett korrekt program ett program som uppfyller sina specifikationer och som är fritt från defekter. Denna avhandling behandlar praktiska verifieringsmetoder applicerade på diagrambaserade modelleringsspråk.

För att vidare undersöka användningen av diagram vid beskrivningen av mellanliggande villkor inom verifieringsmetoden invariantbaserad programmering, har vi konstruerat ett bildbaserat språk för villkor över arrayer. Vi har därefter vidareutvecklat detta språk till ett diagrambaserat domän-specifikt språk (domain-specific language, DSL) och implementerat stöd för det i verifieringsplattformen Why3. Språket låter användaren uttrycka egenskaper hos arrayer, och är baserat på Reynolds intervall- och partitionsdiagram samt inbegriper en konstruktion för mappning av array-intervall till logiska predikat.

Automatisk verifiering av ett program uppnås genom generering av korrekthetsvillkor och åtföljande bevisning av dessa. Särskilt ett exekveringsspår som leder upp till ett falskt mellanliggande villkor utgör ett direkt vederläggande (refutation) av ett bevisvillkor, vilket kräver omedelbar uppmärksamhet från programmeraren. Som ett tillägg till Socos, ett verifieringsverktyg för invariantdiagram baserat på bevissystemet PVS, har vi utvecklat en exekveringsmodell där programmets satser och villkor kan evalueras i ett givet programtillstånd.

Avhandlingen undersöker också visualisering av systemutveckling i samband med modelluppdelning inom Event-B. Uppdelning av en systemmodell blir allt mer kritisk då ett system växer sig större, emedan belastningen på underliggande teorembevisare måste fördelas effektivt.

Masoumeh Parsa är född 1986 i Tehran, Iran. Hon kan vid behov nås per telefon +358 44 974 7123 eller e-post masoumeh.parsa@abo.fi. 

Avhandlingen kan läsas i Åbo Akademis publikationsarkiv Doria. 

Klicka här för pressbild på disputanden.