Information Technology Reference
In-Depth Information
been successfully used in the development of several complex real-life applications. Re-
cently the B method has been extended by the Event B framework [3], which enables
modelling of event-based (reactive) systems. In fact, this extension has incorporated the
action system formalism [6,4] into the B Method.
Event B uses the Abstract Machine Notation for constructing and verifying models.
An abstract machine encapsulates a state (the variables) of the model and provides
operations on the state. A simple abstract machine has the following general form:
MACHINE
AM
VARIABLES
v
INVARIANT
Inv
INITIALISATION
INIT
EVENTS
E
1
...
E
N
The machine is uniquely identified by its name
AM
. The state variables of the machine,
v
, are declared in the
VARIABLES
clause and initialised in
INIT
as defined in the
INITIALISATION
clause. The variables are strongly typed by constraining predicates
of the machine invariant
Inv
given in the
INVARIANT
clause. The invariant is usually
defined as a conjunction of the constraining predicates and the predicates defining the
properties of the system that should be preserved during system execution.
The dynamic behaviour of the system is defined by a set of atomic events specified
in the
EVENTS
clause. An event is defined as follows:
E
=
WHEN
g
THEN
S
END
where the guard
g
is conjunction of the predicates over the machine variables
v
,and
the action
S
is an assignment to state variables. For simplicity, in this paper we do not
consider Event B events with parameters or local variables.
The occurrence of events represents the observable behaviour of the system. The
guard defines the conditions under which the action can be executed, i.e., when the
event is
enabled
. The action can be either a deterministic assignment to the variables or
a non-deterministic assignment from a given set or according to a given postcondition.
The semantics of actions is defined as a before-after (BA) predicate as follows:
Before-after predicate
BA
e
(
x, y, x
)
Action
x
=
E
(
x, y
)
∧
y
=
y
x
:=
E
(
x, y
)
x
=
t
)
∧
y
=
y
x
:
∈
Set
∃
t.
(
t
∈
Set
∧
P
(
x, y, x
)
x
=
t
)
∧
y
=
y
x
:
|
∃
t.
(
P
(
x, t, y
)
∧
where
x
and
y
are disjoint lists (partitions) of state variables, and
x
,y
represent their
values in the after state.
Event B adopts interleaving semantics while treating parallelism. If several events
are enabled then any of them can be chosen for execution non-deterministically. If none
of the events is enabled then the system deadlocks.
To check consistency of Event B machine, we should verify two types of proper-
ties: event feasibility and invariant preservation. Intuitively, event feasibility means that
