Information Technology Reference
In-Depth Information
gluing invariants. Invariants constrain variables, and are supposed to be main-
tained whenever variables are changed by an event. A gluing invariant connects
the abstract variables to the concrete ones. In other words, it glues the state
of the concrete model to that of its abstraction. When just small changes are
applied to a new level of refinement, the abstract model and the concrete model
are similar, so invariants which glue the state of these two models would be
simple. Therefore it can be said that small gaps between refinement levels result
in simple gluing invariants, and simple gluing invariants result in simplicity in
proofs related to them.
3 Atomicity Decomposition in Event-B
This section highlights the motivation for the atomicity decomposition technique
and presents the technique introduced in [7] as a background to development of
our case study.
Although the refinement technique in Event-B provides a flexible approach to
modeling, it does not show all the relations between abstract events and concrete
events. In the atomicity decomposition approach of [7], a graphical technique
is proposed which is intended to make the relationships between abstract and
concrete events clearer and easier to manage than simply using the standard
Event-B refinement method. In this technique course-grained atomicity can be
refined to more fine-grained atomicity. Sub-atomic events are treated in two
ways, some refine abstract events and the others are viewed as hidden events in
abstract level which refine
skip
.
Fig. 2.
Atomicity Decomposition Diagram
The tree structure notation of atomicity decomposition is illustrated in Fig. 2.
In [7] this is called an event refinement diagram. The abstract atomic event,
E1
in this case, appears in the root node, which is decomposed to sub-events in the
next refinement level. There is a sequential control from left to right between
sub-events; in other words, the events, E21, E22, E23 in this figure, are read
from left to right and are executed in this order. One important feature in the
