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

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.