Automated Creation of Safety Cases for Highly Configurable Systems
Tid: Fr 2020-12-04 kl 15.15
Plats: F3, https://kth-se.zoom.us/j/63988855566, Lindstedtsvägen 26, plan 2, Stockholm (English)
Ämnesområde: Maskinkonstruktion
Respondent: Damir Nešić , Mekatronik, Rigorous Systems Engineering
Opponent: PhD Ewen Denney, NASA Ames Research Center
Handledare: Mattias Nyberg, Mekatronik
Abstract
Oavsett domän ökar storleken och komplexiteten hos programvaruintensiva system ständigt. För att tillgodose olika kunders behov konstrueras system oftare som konfigurerbara, där enskilda kunder kan välja den konfiguration som passar dem bäst. Detta innebär att i stället för enstaka system, konstrueras oftare familjer med liknande system. Med tanke på att majoriteten av den nya funktionaliteten kommer från programvara, vars utveckling blir alltmer agil och automatiserad, minskar ledtiderna mellan lanseringarna av nya funktioner och förbättringar. Dessa trender har inte kringgått säkerhetskritiska domäner och som en följd av detta måste aktiviteter för att garantera säkerhet utföras på kortare tid, samtidigt som man hanterar systemfamiljer vars storlek och komplexitet fortsätter att öka. Med tanke på att alla dessa typer av aktiviteter är kända för att vara mödosamma, dokumentationstunga och ofta manuella, är utgångspunkten för denna avhandling att automatisering är nödvändigt för att möjliggöra snabbt utförande av säkerhets relaterade aktiviteter för alltmer komplexa och konfigurerbara system.Denna avhandling presenterar en metod för automatiserat skapande och bedömning av safety case. Safety case är strukturerade, bevisbaserade argument för att ett system är tillräckligt säkert för den avsedda applikationen. Med tanke på fokus på mycket konfigurerbara system, ger den presenterade metoden safety case argumentation för alla möjliga konfigurationer av ett system. Detta uppnås genom att utveckla en allmän och formell modell av konfigurerbara system som stöder sund, kompositionell bevisföring och som gör det möjligt att undvika analys per konfiguration. Villkoren som möjliggör sådan analys används för att definiera en metod för att skapa modulär säkerhetsargumentation. Dess modulära struktur möjliggör oberoende skapande av mindre safety-case-moduler och under vissa förutsättningar, deras sammansättning i större delar av ett safety case. En fördel med den formella grunden är att metoden kan användas för automatisering. Följaktligen presenteras verktygsstöd för skapande av safety case för alla möjliga konfigurationer av ett system. Eftersom safety case alltid är konstruerade i en konkret utveklings-process utformas verktyget genom att identifiera begränsningarna för en typisk industriell utveklings-process. Som en konsekvens fokuserar det presenterade verktyget på informationsmodellering av godtyckliga, men ändå processpecifika artefakter, deras efterföljande automatiserade analys som resulterar i safety-case evidence och slutligen skapandet av safety-case argumentationen. Metoden för skapande av safety case och det utvecklade verktygsstödet utvärderas på två riktiga, konfigurerbara system från fordonstillverkaren Scania, där möjligheten till industriell användning har bekräftats, men också där förslag på ytterligare förbättringar har identifierats.Med tanke på att ett fullständigt safety case alltid kommer att innehåla en viss grad av osäkerhet, presenteras också en halvautomatisk metod för att bedöma graden av osäkerheten. Mer exakt, för fall där det är oklart om det övergripande påståendet i ett safety case är sant, typiskt att "ett system är tillräckligt säkert", presenteras en probabilistisk metod för att beräkna tilltron till ett sådant påstående.Den utvecklade metoden är oberoende av vald safety-case-notation, den baseras på en deterministisk tolkning av godtyckliga säkerhetsargument och den överätts till ett Bayesiskt-nätverk som kan analyseras med godtyckligt verktygs för Bayesiansk nätverkanalys. Metoden utvärderas mot ett benchmark från litteraturen och det visas att till skillnad från tidigare metoder beter sig den presenterade metoden enligt intuitionen, dvs beroende på innehållet i ett safety case är den beräknade sannolikheten som förväntat.