Integrating Stochastic Reasoning Into Event-B Development

A1 Originalartikel i en vetenskaplig tidskrift (referentgranskad)

Interna författare/redaktörer

Publikationens författare: Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis
Förläggare: Springer London
Publiceringsår: 2015
Tidskrift: Formal Aspects of Computing
Volym: 27
Nummer: 1
Artikelns första sida, sidnummer: 53
Artikelns sista sida, sidnummer: 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

Senast uppdaterad 2020-27-01 vid 03:07