Information Technology Reference
In-Depth Information
modify
modify
modifyCodecByDescriptor
respondBySelectortoCodec
modifyBySelector
modify
respondBySelectortoPort
modifyPortByDescriptor
Fig. 9.
Breaking the Atomicity of Modify a Media Channel
5.4 Refinement 3: Breaking the Atomicity of Close Media Channel
This is a simple refinement in which the atomicity of close is broken into two
events (see Fig. 10).
CloseRequest
can be sent by each side of the channel, the
sender of receiver. This figure satisfies the closing requirements shown in the last
phase of Fig. 6.
close
closeRequest
closeAck
closeRequest
closeAck
Fig. 10.
Breaking the Atomicity of Close Media Channel
In Event-B model, by execution of
closeRequest
event, the channel is added
to a set called
closeReqSet
,andthen
closeAck
event is guarded by checking the
set membership of
(ch
∈
closeReqSet)
.
5.5 Assessment
The refinement and atomicity decomposition technique for Event-B of [7] pro-
vides a manageable incremental development of media channel system. The over-
all behaviour of a media channel is modeled abstractly as three atomic events,
establish
,
modify
and
close
. Then each event has been decomposed to sub-events
during refinement levels and details have been added to the model gradually.
The event decomposition is presented by atomicity decomposition diagrams. The
atomicity decomposition technique helps to present the relationships between an
abstract atomic event and concrete sub-events in a hierarchical and sequential
structure and it is specified by some guarded events in Event-B model.
