Predrag Filipovikj försvarar sin doktorsavhandling i datavetenskap

Disputationer och licentiatseminarier

Datum: 2019-06-17
Tid: 13.30
Plats: sal Gamma, MDH Västerås.

Predrag Filipovikj, vid akademin för innovation, design och teknik (IDT), försvarar sin doktorsavhandling i datavetenskap, den 17 juni, klockan 13.30 i sal Gamma, MDH Västerås.

Titel: “Automated Approaches for Formal Verification of Embedded System Artifacts”.

Serienummer: 292

Opponent är professor Jim Woodcock, University of York.

Betygsnämnden utgörs av professor Kim Larsen, Aalborg University, docent Luigia Petre, Åbo Akademi University, docent Christian Berger, Chalmers Tekniska högskola.

Reserv är docent professor Marjan Sirjani, MDH.

Sammanfattning:

Användning av inbyggd programvara for att utföra mycket komplexa funktioner har aktiverats av den ständigt ökande beräkningskraften och minneskapaciteten hos den inbyggda hårdvaran. I bilindustrin har den inbyggda mjukvaran gett trenden "-by-wire", som fokuserar på att ersätta de traditionella mekaniska fordonsfunktionerna med programvaror. Följaktligen har mjukvaran blivit den viktigaste drivkraften för innovation och ett område där konkurrensfördelar uppnås.

Den inbyggda mjukvaran i fordon har blivit så stor och komplicerad att det är svårt att hantera korrektheten hos de relaterade artefakterna, inklusive systemspecifikationerna och designtidsmodellerna, med även de bästa manuella teknikerna. Ett problem beror på det stora antalet,  och  komplicerade,  systemkrav som kombinerar funktionell  och  eventuell  timing  eller andra typer av begränsningar, vilket gör dem svåra att analysera  för att förhindra  spridning av specifikations- och designfel i produktionskoden. Det dominerande sättet att producera programvara är att  använda  det  modellbaserade  paradigmet,  med som Simulink som "de facto" standardverktyg. Simulink-modeller är sålunda viktiga artefakter för inbyggd programvara från vilka kod kan genereras, så att deras korrekthet kan säkerställas. Ett potentiellt sätt att ta itu med  sådana  problem är att tillämpa datorstödda och matematiskt rigorösa specifikations-, analys- och verifieringsmetoder redan vid kravspecifikationen, men också vid senare utvecklingsstadier. Trots den höga automatiseringsgraden samt fullständigheten och noggrannheten i de formella analys-  och  verifieringsmetoder är deras integration med industripraktik fortfarande en utmaning.

För att ta itu med ovan nämnda utmaningar föreslår vi, i denna avhandling, en uppsättning metoder for formell specifikation och analys av systemkrav samt verifiering av designtidsbeteendemodeller av inbyggd programvara som modelleras i Simulink. Våra bidrag som följer är på flera fronter. För det första bedömer vi uttryckligheten hos en befintlig mönsterbaserad teknik för formell kravspecifikation på ett operativt industrisystem. Baserat på  de  positiva resultaten anser vi tekniken uttrycksfull nog för att systematiskt fånga de gemensamma systemens krav, och kompletterar det med ett verktyg som heter PROPAS. Verktyget syftar till att göra det möjligt för utövare att formellt ange sina system. Därefter tillhandahåller vi ett tillvägagångssätt med automatiserad konsistensanalys systemspecifikationerna uttryckta som temporala logikformler. Det föreslagna tillvägagångssättet är helt automatiserat och implementerat i verktyget PROPAS. Det är lämpligt vid systemutvecklings tidiga faser för att felsöka specifikationen. Våra nästa två bidrag gäller formell verifiering och  analys av Simulink-modeller. För att uppnå detta föreslår vi två formella tillvägagångssätt, en baserad på statistisk modellkontroll och den andra på avgränsad modellkontroll, som är skräddarsydd för att hantera storleken och komplexiteten hos industriella Simulink-modeller. Båda metoderna åtföljs av ett adekvat verktygsstöd, nämligen SIMPPAAL och SYMC. För validering tillämpas alla föreslagna tillvägagångssätt på industrisystem som tillhandahålls av våra industripartner Scania och Volvo Group Trucks Technology.

Välkommen!