Augmenting formal development of control systems with quantitative reliability assessment
Anton Tarasyuk, Elena Troubitsynå, Linas Laibinis · 2010
Formal methods, in particular the B Method and its extension Event-B, have demonstrated their value in the development of 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.