Quantitative Reasoning About Dependability in Event-B : Probabilistic Model Checking Approach

Quantitative Reasoning About Dependability in Event-B : Probabilistic Model Checking Approach

Anton Tarasyuk (Åbo Akademi University, Finland & Turku Centre for Computer Science, Finland), Elena Troubitsyna (Åbo Akademi University, Finland) and Linas Laibinis (Åbo Akademi University, Finland)
DOI: 10.4018/978-1-60960-747-0.ch019
OnDemand PDF Download:
No Current Special Offers


Formal refinement-based approaches have proved their worth in verifying system correctness. Often, besides ensuring functional correctness, we also need to quantitatively demonstrate that the desired level of dependability is achieved. However, the existing refinement-based frameworks do not provide sufficient support for quantitative reasoning. In this chapter, we show how to use probabilistic model checking to verify probabilistic refinement of Event-B models. Such integration allows us to combine logical reasoning about functional correctness with probabilistic reasoning about reliability.
Chapter Preview

Introduction To Event-B

The B method (Abrial, 1996) is an approach for the industrial development of highly dependable software. The method has been successfully used in the development of several complex real-life applications. Event-B is a formal framework derived from the B Method to model parallel, distributed and reactive systems. The Rodin platform provides automated tool support for modelling and verification (by theorem proving) in Event-B. Currently Event-B is used in the EU project Deploy (DEPLOY: IST FP7 project, 2008) to model several industrial systems from automotive, railway, space and business domains.

In Event-B a system specification is defined using an abstract (state) machine notion. An abstract machine encapsulates the state (the variables) of a model and defines operations on its state. The general form of an Event-B machine is shown on Figure 1.

Figure 1.

An Event-B machine


The machine is uniquely identified by its name M. The state variables, v, are declared in the Variables clause and initialised in the init event. The variables are strongly typed by the constraining predicates I given in the Invariants clause. The invariant clause might also contain other predicates defining properties that should be preserved during system execution.

The dynamic behaviour of the system is defined by the set of atomic events specified in the Events clause. Generally, an event can be defined as follows:


where the guard g is a conjunction of predicates over the state variables v and the action S is an assignment to the state variables. In its general form, an event can also have local variables as well as parameters. The guard defines the conditions under which the action can be executed, i.e., when the event is enabled. If several events are enabled at the same time, any of them can be chosen for execution non-deterministically. If none of the events is enabled then the system deadlocks.

Complete Chapter List

Search this Book: