Where academic tradition
meets the exciting future

Quantitative Reasoning about Dependability in Event-B: Probabilistic Model Checking Approach

Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis, Quantitative Reasoning about Dependability in Event-B: Probabilistic Model Checking Approach. In: Luigia Petre, Kaisa Sere, Elena Troubitsyna (Eds.), Dependability and Computer Engineering: Concepts for Software-Intensive Systems, 459–472, IGI Global, 2011.

Abstract:

Formal refinement-based approaches have proved their worth in verifying system correctness. Often, besides ensuring functional correctness, we also need quantitatively demonstrate that the desired level of dependability is achieved. However, the existing refinement-based frameworks do not provide sufficient support for quantitative reasoning. In this chapter, we show how to use probabilistic model checking to verify probabilistic refinement of Event-B models. Such integration allows us to combine logical reasoning about functional correctness with probabilistic reasoning about reliability.

BibTeX entry:

@INBOOK{cTaTrLa11a,
  title = {Quantitative Reasoning about Dependability in Event-B: Probabilistic Model Checking Approach},
  booktitle = {Dependability and Computer Engineering: Concepts for Software-Intensive Systems},
  author = {Tarasyuk, Anton and Troubitsyna, Elena and Laibinis, Linas},
  editor = {Petre, Luigia and Sere, Kaisa and Troubitsyna, Elena},
  publisher = {IGI Global},
  pages = {459–472},
  year = {2011},
}

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

Publication Forum rating of this publication: level 1

Edit publication