Integrating Stochastic Reasoning Into Event-B Development

Elena Troubitsyna, Linas Laibinis, Anton Vistbakka

    Research output: Contribution to journalArticleScientificpeer-review

    17 Citations (Scopus)

    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.
    Original languageUndefined/Unknown
    Pages (from-to)53–77
    JournalFormal Aspects of Computing
    Volume27
    Issue number1
    DOIs
    Publication statusPublished - 2015
    MoE publication typeA1 Journal article-refereed

    Keywords

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

    Cite this