Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Integrating Stochastic Reasoni...

Integrating Stochastic Reasoning Into Event-B Development

Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis, Integrating Stochastic Reasoning Into Event-B Development. Formal Aspects of Computing 27(1), 53–77, 2015.

http://dx.doi.org/10.1007/s00165-014-0305-z

Abstract:

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.

BibTeX entry:

@ARTICLE{jTaTrLa14a,
  title = {Integrating Stochastic Reasoning Into Event-B Development},
  author = {Tarasyuk, Anton and Troubitsyna, Elena and Laibinis, Linas},
  journal = {Formal Aspects of Computing},
  volume = {27},
  number = {1},
  publisher = {Springer London},
  pages = {53–77},
  year = {2015},
  keywords = {Event-B; Refinement; Probabilistic reasoning; Reliability; Responsiveness; Cyclic systems; Markov processes},
  ISSN = {0934-5043},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB)

Publication Forum rating of this publication: level 2

Edit publication