Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Facilitating Construction of S...

Facilitating Construction of Safety Cases from Formal Models in Event-B

Yuliya Prokhorova, Linas Laibinis, Elena Troubitsyna, Facilitating Construction of Safety Cases from Formal Models in Event-B. Information and Software Technology 60, 51–76, 2015.

http://dx.doi.org/10.1016/j.infsof.2015.01.001

Abstract:

Context: 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 (informal and formal) are applied to determine the evidence for a safety case. For critical software systems, application of formal methods is often highly recommended for their safety assurance.

Objective: The objective of this paper is to propose a methodology that combines two activities: formalisation of system safety requirements of critical software systems for their further verification as well as derivation of structured safety cases from the associated formal specifications.

Method: We propose a classification of system safety requirements in order to facilitate the mapping of informally defined requirements into a formal model. Moreover, we propose a set of argument patterns that aim at enabling the construction of (a part of) a safety case from a formal model in Event-B.

Results: The results reveal that the proposed classification-based mapping of safety requirements into formal models facilitates requirements traceability. Moreover, the provided detailed guidelines on construction of safety cases aim to simplify the task of the argument pattern instantiation for different classes of system safety requirements. The proposed methodology is illustrated by numerous case studies.

Conclusion: Firstly, the proposed methodology 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, aiming to demonstrate that the safety requirements are indeed met. Consequently, the argumentation used in such a constructed safety case allows us to support it with formal proofs and model checking results used as the safety evidence.

BibTeX entry:

@ARTICLE{jPrLaTr15a,
  title = {Facilitating Construction of Safety Cases from Formal Models in Event-B},
  author = {Prokhorova, Yuliya and Laibinis, Linas and Troubitsyna, Elena},
  journal = {Information and Software Technology},
  volume = {60},
  publisher = {Elsevier},
  pages = {51–76},
  year = {2015},
  keywords = {safety-critical software systems, safety requirements, formal development and verification, Event-B, safety cases, argument patterns},
  ISSN = {0950-5849},
}

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

Publication Forum rating of this publication: level 2

Edit publication