Nesredin Mahmud försvarar sin doktorsavhandling i datavetenskap

Disputationer och licentiatseminarier

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

Nesredin Mahmud, vid akademin för innovation, design och teknik (IDT), försvarar sin doktorsavhandling i datavetenskap, den 13 juni, klockan 13.15 i sal Gamma, MDH Västerås.

Titel: “Design of Assured and Efficient Safety-critical Systems”.

Serienummer: 291

Opponent är professor Joost-Pieter Katoen, RWTH Aachen University.

Betygsnämnden utgörs av professor Peter Csaba Ölveczky, University of Oslo, professor Wolfgang Ahrendt, Chalmers tekniska högskola, docent Raffaela Mirandola, Politecnico di Milano.

Reserv är docent professor Björn Lisper, MDH.

Sammanfattning:

Säkerhetskritiska system bör analyseras noggrant för att ta bort fel i programvaror och specifikationer, dvs systemens krav måste vara entydiga, begripliga och konsekventa, och programvarudesignen ska överensstämma med specifikationerna för att undvika oönskade systemfel. För närvarande saknas effektiva och skalbara metoder för att specificera och analysera systemkrav, och för att formellt analysera beteendemodellerna för inbyggda system. De flesta krav för inbyggda system uttrycks i naturligt språk, vilket är flexibelt och intuitivt men ofta tvetydigt och oprecist. Förutom naturligt språk används ofta mallbaserade kravspecifikationsmetoder för att specificera krav (speciellt i säkerhetskritiska tillämpningar). Även om de senare minskar otydligheten och förbättrar begripligheten, är de vanligtvis oflexibla på grund av den begränsade syntaxen i mallarna, och mallvalet är svårt. Industriella system utvecklas ofta genom att använda modellerings- och simuleringsmiljöer såsom Simulink, som också används för att generera kod automatiskt för olika hårdvaruplattformar. Därför är det viktigt att kunna formellt analysera Simulink-modeller, för att få insikt i beteendet hos det inbyggda systemet, och för att förhindra potentiella fel från att sprida sig till implementationen. Att analysera tidsperspektivet för sådan säkerhetskritisk mjukvara som har tasks med olika periodicitet och som har begränsningar på datas ålder, dvs datans färskhet, för end-to-end-programvarufunktionalitet, är inte trivialt. Detta orsakas av undersamplings- och översamplingseffekter, som uppstår när data går från högre till lägre signaleringshastigheter och vice versa. Vidare, när sådana system används i en distribuerad arkitektur, t.ex. elektriska / elektroniska fordonssystem, , så bör, förutom att säkerställa tidskraven, även tillförlitligheten hos den distribuerade mjukvaran maximeras för att motverka den högre risken för fel i den distribuerade databehandlingen, för att därigenom förbättra den övergripande förutsägbarheten för det säkerhetskritiska systemet. Design för tillförlitlighet kräver emellertid vanligtvis mer av kritiska systemresurser, såsom energi. För att tillgodose nuvarande och framtida mjukvarufunktionalitet bör utformningen av det säkerhetskritiska systemet ta hänsyn till effektiviteten hos kritiska systemresurser, såsom energiförbrukning, samtidigt som kraven på tid och tillförlitlighet uppfylls.

För att möta ovanstående behov, föreslår vi i denna avhandling formella metoder och optimeringstekniker för att säkerställa förbättrad kvalitet på kravspecifikationer och mjukvaruutveckling, och för att effektivt mappa mjukvarufunktionalitet till hårdvara. Avhandlingens bidrag är: (i) ReSA - ett domänspecifikt språk för kravspecifikation, skräddarsytt för inbyggda system, baserat på begränsat naturligt språk; (ii) ett formellt tillvägagångssätt för att kontrollera konsistensen av ReSA-specifikationer genom SAT och Ontologi; (iii) ett ramverk baserat på statistisk modellkontroll för att analysera Simulink-modeller via automatiserad omvandling till nätverk av stokastiska tidsautomater; och (iv) en resurseffektiv fördelning av feltolerant programvara med end-to-end-tidskrav och driftsäkerhetsbegränsningar genom heltals-linjär programmering och hybrid partikel-svärmoptimering. Våra föreslagna lösningar utvärderas i fall som används i fordon, såsom justerbar hastighetsbegränsare (ASL) och BBW-system från Volvo Group Trucks Technology (VGTT), och på ett motorstyrsystem från Bosch.

Välkommen!