Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Towards Rigorous Construction ...

Towards Rigorous Construction of Safety Cases

Yuliya Prokhorova, Linas Laibinis, Elena Troubitsyna, Towards Rigorous Construction of Safety Cases. TUCS Technical Reports 1110, Turku Centre for Computer Science, 2014.

Abstract:

Certification of safety-critical software systems requires submission of safety assurance documents, e.g., in the form of safety cases. A safety case is a justification argument used to show that a system is safe for a particular application in a particular environment. Different argumentation strategies are applied to determine the evidence for a safety case. They allow us to support a safety case with such evidence as results of hazard analysis, testing, simulation, etc. On the other hand, application of formal methods for development and verification of critical software systems is highly recommended for their certification. In this paper, we propose a methodology that combines these two activities. Firstly, it allows us to map the given system safety requirements into elements of the formal model to be constructed, which is then used for verification of these requirements. Secondly, it guides the construction of a safety case demonstrating that the safety requirements are indeed met. Consequently, the argumentation used in such a safety case allows us to support the safety case with formal proofs and model checking results as the safety evidence. Moreover, we propose a set of argument patterns that aim at facilitating the construction of (a part of) a safety case from a formal model. In this work, we utilise the Event-B formalism due to its scalability and mature tool support. We illustrate the proposed methodology by numerous small examples as well as validate it by a larger case study – a steam boiler control system.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tPrLaTr14a,
  title = {Towards Rigorous Construction of Safety Cases},
  author = {Prokhorova, Yuliya and Laibinis, Linas and Troubitsyna, Elena},
  number = {1110},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2014},
  keywords = {safety-critical software systems, safety requirements, formal development, formal verification, Event-B, safety cases, argument patterns},
  ISBN = {978-952-12-3064-6},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB)

Edit publication