• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Augmenting Formal Development of Control Systems with Quantitative Reliability Assessment

Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis, Augmenting Formal Development of Control Systems with Quantitative Reliability Assessment. In: Proceedings of 2nd Int. Workshop on Software Engineering for Resilient Systems - SERENE 2010, ACM, 2010.

Abstract:

Formal methods, in particular the B Method and its extension Event-B, have proved their worth in the development of many complex control systems. However, while providing us with a powerful development platform, these frameworks poorly support quantitative assessment of dependability attributes. Yet, by assessing dependability at the early design phase we would facilitate development of systems that are not only correct-by-construction but also achieve the desired dependability level. In this paper we demonstrate how to integrate reliability assessment performed via Markov analysis into refinement 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
provably correct but also have a required level of reliability.

BibTeX entry:

@INPROCEEDINGS{inpTaTrLa10a,
  title = {Augmenting Formal Development of Control Systems with Quantitative Reliability Assessment},
  booktitle = {Proceedings of 2nd Int. Workshop on Software Engineering for Resilient Systems - SERENE 2010},
  author = {Tarasyuk, Anton and Troubitsyna, Elena and Laibinis, Linas},
  publisher = {ACM},
  year = {2010},
  keywords = {Reliability assessment, formal modelling, Event-B, Markov processes, refinement, probabilistic model checking},
}

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

Edit publication