Information Technology Reference
In-Depth Information
execution of an event from any state where both the machine invariant and the event
guard hold is possible, i.e., it can produce at least one state that satisfies the before-after
predicate, i.e.,
v
.BA
e
(
v, v
)
The invariant preservation property simply states that invariant should be maintained:
G
e
(
v
)
⇒∃
Inv
(
v
)
∧
Inv
(
v
)
The main development methodology of Event B is refinement - the process of trans-
forming an abstract specification while preserving its correctness and gradually intro-
ducing implementation details. Let us assume that the refinement machine
AM
BA
e
(
v, v
)
⇒
Inv
(
v
)
∧
G
e
(
v
)
∧
is a
result of refinement of the abstract machine
AM
:
MACHINE
AM
VARIABLES
w
INVARIANT
Inv
INITIALISATION
INIT
EVENTS
E
1
...
E
M
In
AM
we replace the abstract variables of
AM
(
v
) with the concrete ones (
w
). The
invariant of
AM
-
Inv
- defines now not only the invariant properties of the refined
model, but also the connection between the newly introduced variables (
w
)andthe
abstract variables that they replace (
v
). For a refinement step to be valid, every possible
execution of the refined machine must correspond (via
Inv
) to some execution of the
abstract machine. To demonstrate this, we should establish two facts - feasibility of
refined events and their correctness with respect to the abstract events. To demonstrate
feasibility, we should prove the following:
Inv
(
v
)
∧
w
.BA
e
(
w, w
)
where
G
(
w
)
is the guard of the refined event and
BA
(
w, w
)
its before-after predicate.
To demonstrate that each event is a correct refinement of its abstract counterpart, we
should first prove that the guard is strengthened in the refinement:
Inv
(
v
)
∧
Inv
(
v, w
)
∧
G
e
(
w
)
⇒∃
Inv
(
v, w
)
∧
G
e
(
w
)
⇒
G
e
(
v
)
Finally, we need to demonstrate a correspondence between the abstract and concrete
postconditions:
Inv
(
v, w
)
∧
G
e
(
w
)
∧
BA
e
(
w, w
)
⇒∃
v
.
(
BA
e
(
v, v
)
∧
Inv
(
v
,w
))
Inv
(
v
)
∧
The refined model can also introduce new events. In this case, we have show that these
new events are refinements of implicit empty (skip) events of the abstract model.
While presenting Event B above, we have slightly simplified matters by omitting the
fact that Event B model consists of two separate parts. The static part, called
c
ontext,
contains the declaration of new types(sets), constants and axioms. The presented, dy-
namic part (machine) contains the variable declarations and events. However, this sim-
plification is of syntactic nature and is insignificant as such. Our approach to refinement
pattern definition that we are presenting next can be easily extended to compensate it.
