Automated Creation of Safety Cases for Highly Configurable Systems

Regardless of the domain, the size and complexity of software-intensive systems is constantly increasing. At the same time, to satisfy the needs of different customers, systems are more frequently being engineered as configurable, where individual customers can select the configuration that suits them best. Effectively, this means that instead of single systems, more frequently families of similar systems are being engineered. Furthermore, given that the majority of novel functionality is coming from software, whose development is increasingly agile and automated, the lead times between the releases of new features and improvements is reducing. These trends have not bypassed safety-critical domains, and as a consequence, safety-assurance activities must be performed in shorter time, while dealing with families of systems whose size and complexity keeps increasing. Given that any type of assurance is notorious for being laborious, documentation-heavy, and often manual, the conjencture of this thesis is that automation is necessary to enable timely execution of assurance activities for increasingly complex, and configurable systems. This thesis presents a method for automated creation and assessment of safety cases, which are structured, evidence-supported arguments that a system is sufficiently safe for the intended application. Given the focus on highly configurable systems, the presented method yields safety-case argumentation for all possible configurations of a system. This is achieved by developing a general, and formal model of configurable-systems which supports sound, compositional reasoning, and which allows avoiding per-configuration analysis. The conditions that enable such compositional analysis are used to define a method to create modular safety-case argumentation. Its modular structure allows independent creation of smaller safety-case modules, and under certain conditions, their composition into larger parts of a safety case. A benefit of the formal foundation is the fact that the method is amenable to automation. Consequently, tool-support for the creation of evidence-supported safety-case argumentation for all possible configurations of a system is presented. Because safety-cases are always constructed in a concrete engineering process, the tool is designed by identifying the constraints of a typical, industrial, engineering process. As a consequence, the presented tool focuses on information-modeling of arbitrary, yet engineering-process-specific artifacts, their subsequent automated analysis that results in safety-case evidence, and finally the creation of the safety-case argumentation. The method for safety-case creation, and the developed tool-support, are evaluated on two real, configurable systems from the heavy-vehicle manufacturer \textsc{Scania}, where the feasibility of industrial adoption has been confirmed, but also where suggestions for further improvements have been identified. Given that a complete safety-case will always encode some degree of uncertainty, a semi-automated method to asses the degree of the encoded uncertainty is also presented. More precisely, for cases when it is unclear if the overall claim of a safety case is true, typically that "a system is sufficiently safe", a probabilistic method to calculate the belief in such claim is presented. The developed method is it is safety-case-notation independent, it is underlined by a deterministic interpretation of arbitrary safety-case arguments, and it is encoded as a Bayesian Network that can be analyzed with off-the-shelf tool support. The method is evaluated against a benchmark from the literature and it is shown that unlike previous methods, the presented method behaves according to the intuition, i.e. depending on the content of a safety case the calculated belief values are as expected.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