kth.sePublications KTH
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Automated Creation of Safety Cases for Highly Configurable Systems
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics. (Rigorous Systems Engineering)ORCID iD: 0000-0003-4557-2849
2020 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

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.

Abstract [sv]

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.

Place, publisher, year, edition, pages
KTH Royal Institute of Technology, 2020. , p. 269
Series
TRITA-ITM-AVL ; 2020:44
National Category
Embedded Systems
Research subject
Machine Design
Identifiers
URN: urn:nbn:se:kth:diva-285813ISBN: 978-91-7873-707-9 (print)OAI: oai:DiVA.org:kth-285813DiVA, id: diva2:1499900
Public defence
2020-12-04, F3, https://kth-se.zoom.us/j/63988855566, Lindstedtsvägen 26, plan 2, Stockholm, 15:15 (English)
Opponent
Supervisors
Funder
Vinnova, 2015-02441, 2016-02804, 2018-01778Available from: 2020-11-13 Created: 2020-11-10 Last updated: 2022-09-13Bibliographically approved
List of papers
1. Product-Line Assurance Cases from Contract-Based Design
Open this publication in new window or tab >>Product-Line Assurance Cases from Contract-Based Design
(English)Manuscript (preprint) (Other academic)
Abstract [en]

Assurance cases are used to argue in a structured, and evidence-supported way, that a property such as safety or security is satisfied by a system. In some domains however, instead of single systems, product lines with many system-variants are engineered, to satisfy the needs of different customers. In such context, single-system methods for assurance-case creation suffer from scalability issues because the underlying assumption is that the evidence and arguments can be created per system variant. This paper presents a novel method for product-line assurance-case creation where all the arguments and the evidence are created without analyzing each system variant. Consequently, the effort to create an assurance case scales with the complexity of system variants, instead with their number. The method is based on a contract-based design framework for cyber-physical systems, which is extended to define the conditions under which all system variants satisfy a particular property. These conditions are used to define an assurance-case pattern, which can be instantiated for arbitrary product lines. Moreover, the defined pattern is modular to enable step-wise assurance-case creation. Finally, an exploratory case study is performed on a real product-line from the heavy-vehicle manufacturer Scania to evaluate the applicability of the presented method.

Keywords
Assurance cases, Product line engineering, Contract-based design.
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-285808 (URN)
Funder
Vinnova, 2018-01778
Available from: 2020-11-10 Created: 2020-11-10 Last updated: 2022-06-25Bibliographically approved
2. A Probabilistic Model of Belief in Safety Cases
Open this publication in new window or tab >>A Probabilistic Model of Belief in Safety Cases
(English)Manuscript (preprint) (Other academic)
Abstract [en]

A safety case is a hierarchical argument supported by evidence, whose scope is defined by contextual information. The goal is to show that the conclusion of such argument, typically "the system is acceptably safe", is true. However, because the knowledge about systems is always imperfect, the value true cannot be assigned with absolute certainty. Instead, researchers have proposed to assess the belief that a conclusion is true, which should be high for a safe system. Existing methods for belief calculations suffer from various limitations that lead to unrealistic belief values. This paper presents a novel method, underlined by formal definitions of concepts such as conclusion being true, or context defining the scope. Given these definitions, a general, probabilistic model for calculating the belief in a conclusion of an arbitrary argument is derived. Because the derived probabilistic model is independent of any safety-case notation, the elements of a commonly used notation are mapped to the formal definitions, and the corresponding probabilistic model is represented as a Bayesian Network to enable large-scale calculations. Finally, the method is applied to scenarios where previous methods produce unrealistic values, to show that the presented method produces belief values as expected.

Keywords
Safety case, Safety-case representation, Reasoning under uncertainty, Model Theory, Bayesian Network
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-285809 (URN)
Funder
Vinnova, 2018-01778
Note

Submitted to the Elsevier Journal on Safety Science

Available from: 2020-11-10 Created: 2020-11-10 Last updated: 2022-06-25Bibliographically approved
3. Tool-supported generation of safety cases for highly configurable systems
Open this publication in new window or tab >>Tool-supported generation of safety cases for highly configurable systems
(English)Manuscript (preprint) (Other academic)
Abstract [en]

An increasing number of standards are recommending a safety case to argue that a particular safety-critical system is acceptably safe. However, to satisfy the needs of different customers, companies are instead engineering families of safety-critical system by making them configurable. Due to the complexity of safety cases, which is only increased when arguing about a family of systems, creating safety cases without some level of automation is a manual, error-prone activity. Existing tools suffer from conceptual limitations, e.g. inability to manage large system families, or from practical limitations, e.g. they require specific artifacts in specific formats. In other words, general tool-support for automated generation of safety-case argumentation is missing. To overcome this limitation, empirical studies are analyzed to characterize the typical industrial context, and then general requirements are synthesized for a general tool for automated safety-case creation. Guided by the elicited requirements, a concrete tool for automated safety-case construction is presented. The tool was developed in collaboration with the heavy-vehicle manufacturer Scania, and with the underlying idea that the tool should be generic, but possible to tailor to different organizations, and methods for the creation of safety-case argumentation. The key idea is that the tailoring is performed in a declarative way, by simply expressing the entities and constraints that the tool should enforce. The feasibility of using the created tool is evaluated by generating safety-case argumentation for a safety-critical, highly configurable system from Scania. Although further validation is needed, the findings indicate that industrial adoption is feasible.

Keywords
Safety Case, Configurable System, Product Line, Information Modeling
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-285811 (URN)
Funder
Vinnova, 2018-01778
Note

Submitted to the Springer journal on Automated Software Engineering

Available from: 2020-11-10 Created: 2020-11-10 Last updated: 2022-06-25Bibliographically approved

Open Access in DiVA

fulltext(1001 kB)558 downloads
File information
File name FULLTEXT01.pdfFile size 1001 kBChecksum SHA-512
812444466b21bcd892930566516ccfc09bc3dcf71ff3d7fb29a3fb480fb033bf1727db3242c35393bdc0a4a52e500076678c6fd6dd8466842b4ae9889a23d0bd
Type fulltextMimetype application/pdf

Other links

http://Vid fysisk närvaro eller Du som saknar dator/ datorvana kan kontakta service@itm.kth.se (English)

Search in DiVA

By author/editor
Nešić, Damir
By organisation
Mechatronics
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 558 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 1415 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf