Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Quantitative Verification of S...

Quantitative Verification of System Safety in Event-B

Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis, Quantitative Verification of System Safety in Event-B. In: Elena Troubitsyna (Ed.), Proceedings of SERENE 2011, The 3rd International Workshop on Software Engineering for Resilient Systems, Lecture Notes in Computer Science, 24–39, Springer , 2011.

Abstract:

Certification of safety-critical systems requires formal verification of system properties and behaviour as well as quantitative demonstration of safety. Usually, formal modelling frameworks do not include quantitative assessment of safety. This has a negative impact on productivity and predictability of system development. In this paper we present an approach to integrating quantitative safety analysis into formal system modelling and verification in Event-B. The proposed approach is based on an extension of Event-B, which allows us to perform quantitative assessment of safety within proof-based verification of system behaviour. This enables development of systems that are not only correct but also safe by construction. The approach is demonstrated by a case study -- an automatic railway crossing system.

BibTeX entry:

@INPROCEEDINGS{iTaTrLa11a,
  title = {Quantitative Verification of System Safety in Event-B},
  booktitle = {Proceedings of SERENE 2011, The 3rd International Workshop on Software Engineering for Resilient Systems},
  author = {Tarasyuk, Anton and Troubitsyna, Elena and Laibinis, Linas},
  series = {Lecture Notes in Computer Science},
  editor = {Troubitsyna, Elena},
  publisher = {Springer },
  pages = {24–39},
  year = {2011},
  keywords = {Event-B, refinement, safety, probability},
}

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

Publication Forum rating of this publication: level 1

Edit publication