Aspect-Oriented Formal Specification for Real-Time Systems - Advances in Computational Science and Engineering - page 22

The Medium Aspect
The unreliable medium is the last aspect that requires definition. This agent will form
the connection between the sending and the receiving aspects. One can infer from the
definitions of these aspects that this agent must have ports labeled { send 0 , send 1 ,ack 1 ,
a 0 , a 1 , recu 0 , recu 1 }. Also remember that this aspect has to non-deterministically
loose messages. Suppose that the specification is[28] :
Weaving Three Aspects Together into a Single Framework
Having defined the aspects involved in the ABP, all that remains (for the modeling
task) is to weave them together in order to form the larger protocol. This is done with
two compositions[28] :
This defines the ABP to be a composition of S and M, interacting on channels send 0 ,
send 1 , ack 0 , acka 1 }, and a composition of M and R interacting on channels { recu 0 ,
recu 1 , a 0 , a 1 }. Finally, ABP entire Specification is formed[28] :