Where academic tradition
meets the exciting future

From Formal Specification in Event-B to Probabilistic Reliability Assessment

Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis, From Formal Specification in Event-B to Probabilistic Reliability Assessment. In: Proceedings of DEPEND 2010, the 3rd International Conference on Dependability, IEEE Computer Society's Conference Publishing Services, 2010.

Abstract:

Formal methods, in particular the B Method and its extension Event-B, have proven their worth in the development of many complex software-intensive systems. However, while providing us with a powerful development platform, these frameworks poorly support quantitative assessment of dependability attributes. Yet, such an assessment would facilitate not only system certification but also system development by guiding it towards the design optimal from the dependability point of view. In this paper we demonstrate how to integrate reliability assessment performed by model checking into refinement process in Event-B. Such an integration allows us to combine logical reasoning about functional correctness with probabilistic reasoning about reliability. Hence we obtain a method that enables building the systems that are not only correct-by-construction but also have a predicted level of reliability.

BibTeX entry:

@INPROCEEDINGS{inpTaTrLa10b,
  title = {From Formal Specification in Event-B to Probabilistic Reliability Assessment},
  booktitle = {Proceedings of DEPEND 2010, the 3rd International Conference on Dependability},
  author = {Tarasyuk, Anton and Troubitsyna, Elena and Laibinis, Linas},
  publisher = {IEEE Computer Society's Conference Publishing Services},
  year = {2010},
}

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

Edit publication