Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Supporting Formal Modelling in...

Supporting Formal Modelling in Event-B with Safety Cases

Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis, Supporting Formal Modelling in Event-B with Safety Cases. In: Michael Butler, Stefan Hallerstede, Marina Waldén (Eds.), Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes 18, 8–11, TUCS, 2013.

Abstract:

Nowadays safety cases and the supporting graphical argumentation notation called Goal Structuring Notation (GSN) are widely adopted in the certification process of safety-critical systems. The safety cases allow us to justify why a system is safe and whether the design adequately incorporates the safety requirements defined in a system requirements specification. Moreover, there is a growing tendency to support a safety case with an evidence generated from formal analysis. Formal proofs provide justification for the validity of claims and, as such, are increasingly widely deployed in software development. However, formal proofs as an evidence are only reasonable if those proofs are demonstrated to validate the incorporated safety requirements. In this paper, we extend our previous work on linking of modelling in Event-B with safety cases. We give an extended classification of safety requirements and define how each class can be represented in a formal specification. We utilise the Event-B framework to automatically generate proof obligations, which can be then used in a safety case as the evidence that requirements have been met. The approach permits the developers to obtain a consistent system specification that allows for derivation of a sufficient safety case.

BibTeX entry:

@INPROCEEDINGS{inpPrTrLa13a,
  title = {Supporting Formal Modelling in Event-B with Safety Cases},
  booktitle = {Proceedings of the 4th Rodin User and Developer Workshop},
  author = {Prokhorova, Yuliya and Troubitsyna, Elena and Laibinis, Linas},
  volume = {18},
  series = {TUCS Lecture Notes},
  editor = {Butler, Michael and Hallerstede, Stefan and Waldén, Marina},
  publisher = {TUCS},
  pages = {8–11},
  year = {2013},
  keywords = {Event-B, formal proofs, safety requirements, safety cases},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication