Information Technology Reference
In-Depth Information
structure is the distinction between solid lines and dashed lines. The sub-event
corresponding to dashed line, E21, E22, are new events which refine
skip
in the
abstract level. The child node with a solid line, E23, is a main event which
should be proved to refine the abstract one, E1. The hierarchical and sequential
structure is influenced by the structure diagrams of Jackson System Development
(JSD) [13].
In this case, E21, E22 should execute before E23 in order to reach a state that
enables event E23. This is done by some control variables in Event-B model.
An Event-B model of this diagram is illustrated in Figs. 3, 4 and 5. VarE21,
VarE22 and VarE23 are control variables. Event E22 is guarded by VarE21 which
indicates the sequential execution of E21 and E22. Also event E23 is guarded
by VarE22. Event E23 can be executed only when E22 has been executed, and
event E22 can be executed only when E21 has been executed.
The possible execution traces of the model are presented here. The only event
trace in abstract machine, which contains abstract event E1, is
<E
>
and the execution of E21, E22, and E23 is given by the only trace of the refined
model:
<E
1
>
The event refinement diagram is used because it explicitly illustrates our inten-
tion that the effect achieved by E1 at the abstract level is realized at the refined
level by execution of E21 followed by E22 followed by E23. In the standard
Event-B method E21 and E22 are refinements of
skip
and there is no explicit
connection to E1. Technically, E23 is the only event that refines E1 but the
diagram indicates that we break the atomicity of E1 into events E21, E2 and
E23.
21
,E
22
,E
23
Fig. 3.
Event-B Model Part a
Atomicity decomposition has been applied to a distributed file system in [7].
It can be used for many types of system, including sequential, concurrent and
distributed systems. It is important to note that the technique of using refine-
ment of
skip
is standard in action systems [9] and Event-B [1] and its use can
also be found in Z refinement [11].
