Skip to main content
To KTH's start page To KTH's start page

Automated Creation of Safety Cases for Highly Configurable Systems

Time: Fri 2020-12-04 15.15

Location: F3,, Lindstedtsvägen 26, plan 2, Stockholm (English)

Subject area: Machine Design

Doctoral student: Damir Nešić , Mekatronik, Rigorous Systems Engineering

Opponent: PhD Ewen Denney, NASA Ames Research Center

Supervisor: Mattias Nyberg, Mekatronik

Export to calendar


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.