Information Technology Reference
In-Depth Information
2 Event-B Background
Event-B [1, 2] is a formal method for specifying, modeling and reasoning about
systems. Event-B has evolved from Classical B [8] and Action Systems [9]. Key
features of Event-B are modeling and reasoning. The modeling notation is based
on set theory and predicate logic. Building a model in Event-B typically starts
with a very abstract level, and continues in different levels by use of refine-
ment technique. Event-B use mathematical proof to verify consistency between
refinement levels.
An Event-B model [1, 10] consists of
contexts
and
machines
.Inotherwords,
a model is made of several components of these two types. Contexts contain
the static part of a model while a machines contain the dynamic part. There
are various relationships between contexts and machines. A context can be “ex-
tended” by other contexts and “referenced” or “seen” by machines. A Machine
can be “refined” by other machines and refers to contexts as its static part. The
structure is shown in Fig. 1.
Fig. 1.
Event-B Structure
Building a model usually starts with a very abstract model of the system,
and then gradually details are added through several modeling steps in such a
way that leads us towards a suitable implementation; this approach is called
refinement [3, 4]. Thus, instead of building a single model in a flat manner, we
have a sequence of models, where each of them is supposed to be a refinement
of the previous.
From a given model M1, a new model M2 can be built as a refinement of M1.
In this case, model M1 is called an abstraction of M2, and model M2 is said to
be a concrete version of M1. A concrete model is said to refine its abstraction.
Each event of a concrete machine refines an abstract event or refines
skip
.An
event that refines
skip
is referred to as a new event since it has no counterpart
in the abstract model.
In the introduction we stated that small gaps between refinement levels re-
sults in simplicity in proof obligations. Most of proof obligations are related
to consistency between refinement levels. Ensuring consistency is done by some
