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

Fig. 2. Weaving Aspects into Automata
3.2 Aspect Oriented Formal Specification of ABP
The alternating bit protocol (hereafter ABP)[27][28] is a well-known protocol for
communication between two parties over an unreliable loss medium (e.g. Ethernet).
Briefly, each message that is sent over the medium has a single bit added, either a 1 or
a 0. This bit can be used to determine if this message is a duplicate (perhaps re-sent
after an acknowledgement was not received after a pre-determined amount of time).
By the same token, this also allows the sender to determine if an acknowledgement
just received is a duplicate (imagine the case where one message was sent, but the
acknowledgement was delayed. The sender re-sends the message, and another ac-
knowledgement was sent. Acknowledgement one arrives, so the next message is sent.
If the delayed acknowledgement is received, the sender may otherwise assume that
the message it just sent was received).
In this protocol, the loss of whole messages is possible. Corruption is possible over
physical medium, but this does not form part of the protocol (the receiver can always
drop a corrupted message if it is determined to be corrupted by some higher level
protocol), and neither does reordering of messages. This should be reflected in the
model.
For simplify the specification of ABP, the ABP protocol is divided into three as-
pects: the sending aspect, receiving aspect and the medium aspect, each aspect can be
specified separately, finally we weave the three aspects into a single specification
framework. Process algebras are a set of mathematically rigors languages with well
defined operational semantics that allow for proofs of systems and propositions, either
in terms of drawing an isomorphism between two systems such that they can be said
to be equivalent, or in terms of deriving a system from its base terms. Process alge-
bras CCS[[8] and PEPA[27] [29] are presented as modeling languages for concurrent