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. I synnerhet är analys inte trivial av timing-beteendet 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 över input-output-kommunikationsvägar. 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 den säkerhetskritiska mjukvaran används på 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 den växande komplexiteten i 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.

I denna avhandling föreslår vi formella metoder och optimeringstekniker för att säkerställa förbättrad kvalitet på kravspecifikationer och mjukvaruutveckling, och att effektivt mappa mjukvarufunktionalitet till hårdvara. Bidrag i avhandlingen är: (i) ett avgränsande kravspecifikationsspråk för inbyggda system, ReSA; (ii) en formell analys av ReSA-specifikationer via SMT och Ontologi; iii) En statistisk modellkontroll av en mjukvarukonstruktion, modellerad i Simulink via transformation till ett nätverk av stokastiska tidsautomater; (iv) En resurseffektiv fördelning av feltolerant programvara med end-to-end-tidskrav och driftsäkerhetsbegränsningar genom heltals-linjär programmering och hybridpartikel-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!