Information Technology Reference
In-Depth Information
Fig. 13.
Weak Sequencing Diagram with guard line
that according to requirements we would want to force them to be executed in a
specific ordering, we insert a guard line between them. The inserted guard line
means
ReceiveM1
should be executed before
SendM2
.
6.3 Weak Sequencing in the Media Channel Model
In our model of the media channel system the weak sequencing interpretation
is used in further decomposition of the
close
event. As shown in Fig. 6,
receive-
CloseRequest
should execute before
sendCloseAck
. This constraint is illustrated
by a guard line in Fig. 14. It means that for sending the close acknowledge signal,
a close request should be received before.
This guard line influences the Event-B model by adding a new guard to the
sendCloseAck
event requiring prior execution of the
receiveCloseRequest
event.
close
closeRequest
closeAck
sendCloseRequest
receiveCloseRequest
sendCloseAck
receiveCloseAck
Fig. 14.
Weak Sequencing Diagram in Decomposing Close Event
7 Conclusion and Directions for Future Work
An explicit representation of the sequencing of sub-events and refinement re-
lationships, called atomicity decomposition has been used and assessed. The
hierarchical diagrams introduce control structure in an incremental modeling of
a case study. In abstraction media channel requirements are considered as three
phases, establish, modify and close. In this paper we have shown that how each
phase refine to detailed refinement using the benefits of atomicity decomposition
technique in structuring requirements.
