Integrating Stochastic Reasoning Into Event-B Development

A1 Journal article (refereed)

Internal Authors/Editors

Publication Details

List of Authors: Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis
Publisher: Springer London
Publication year: 2015
Journal: Formal Aspects of Computing
Volume number: 27
Issue number: 1
Start page: 53
End page: 77
eISSN: 1433-299X


Dependability is a property of a computer system to deliver services that can be justifiably trusted. Formal modelling and verification techniques are widely used for development of dependable computer-based systems to gain confidence in the correctness of system design. Such techniques include Event-B — a state-based formalism that enables development of systems correct-by-construction. While Event-B offers a scalable approach to ensuring functional correctness of a system, it leaves aside modelling of non-functional critical properties, e.g., reliability and responsiveness, that are essential for ensuring dependability of critical systems. Both reliability, i.e., the probability of the system to function correctly over a given period of time, and responsiveness, i.e., the probability of the system to complete execution of a requested service within a given time bound, are defined as quantitative stochastic measures. In this paper, we propose an extension of the Event-B semantics to enable stochastic reasoning about dependability-related non-functional properties of cyclic systems. We define the requirements that a cyclic system should satisfy and introduce the notions of reliability and responsiveness refinement. Such an extension integrates reasoning about functional correctness and stochastic modelling of non-functional characteristics into the formal system development. It allows the designer to ensure that a developed system does not only correctly implement its functional requirements but also satisfies given non-functional quantitative constraints.


Event-B, Markov processes, probabilistic reasoning, refinement, reliability, Responsiveness

Last updated on 2020-04-06 at 03:53