Patterns for Refinement Automation - Formal Methods for Components and Objects - page 100

Up to the fourth level of refinement of the media channel system, the basic
sequential atomicity decomposition of the diagrammatic notation was sucient
for decomposing events and adding details to the model. However in the fourth
level we identified some extensions to the notation that were convenient for
representing further aspects of the atomicity decomposition. These are covered
in the next section.
6 Extending the Diagrammatic Notation
6.1 Case Splitting Pattern
We found it convenient to introduce a diagrammatic notation to represent case
splitting in a refinement. With the case splitting notation, an event is split to
several sub-events is a way that execution of the abstract event is realized by
execution of any of the refined events. It is presented by a circle containing
an “or”, as can be seen in Fig. 11. Jackson's JSD diagrams also includes case
splitting [13].
modify
modifyBySelector
modifyCodecByInitiator modifyCodecByAcceptor
Fig. 11. Case Splitting, Level 4 of Refinement
In our model the case splitting is achieved by adding only one guard to each
refined event which constrains the direction of the media channel. If the direction
is from initiator to acceptor, ItoA , only the Initiator can modify the codec,
because it has received the list of codecs belonging to acceptor, so can choose a
new codec whenever it wants; and if the direction is from acceptor to initiator,
AtoI , the one which has received the list of codecs is acceptor, so in this case it
may modify the codec.
6.2 Weak Sequencing and Guard Lines
Consider the diagram in Fig. 12(a) where abstract event X is sequentially split
into events M1 and M2 and where M1 and M2 are respectively further refined
into sequential sub-events. Clearly, in abstract level M2 occurs after M1 ,and
in the next level ReceiveM1 occurs after SendM1 and ReceiveM2 occurs after
SendM2 .Since ReceiveM1 refines M1 and ReceiveM2 refines M2 ,and M2 occurs
after M1 , clearly ReceiveM2 occurs after ReceiveM1 , i.e., the ordering constraint