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. TUCS Technical Reports 1010, Turku Centre for Computer Science, 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.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tTaTrLa11b,
  title = {Quantitative Verification of System Safety in Event-B},
  author = {Tarasyuk, Anton and Troubitsyna, Elena and Laibinis, Linas},
  number = {1010},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2011},
  keywords = {Event-B, refinement, safety, probability},
}

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

Edit publication