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

systems and protocols, and are given a formal definition. PEPA is presented with a
worked example of the alternating bit protocol, and it is demonstrated how equiva-
lence relations may be drawn to prove functional and behavioral properties of this
protocol, and how mathematically sound performance analysis can be applied using
tools associated with this language. The methodology presented here is a generic one,
and could easily be applied to other systems and may be considered a framework for
modeling, proving and evaluating performance of other network protocols, as well as
any concurrent and cooperating system.
One of the features of most process algebras is the facility to compose systems
from specifications of individual aspects. As we will see, this is a useful feature.
Within the ABP there are three distinct aspects to consider. Therefore, the modeling
task should consider each of these in turn and then weave them all together to form
the whole protocol.
The Sending Aspect
It is presumed that the sending aspect of the protocol will sit between some higher-
level application and the physical medium. Therefore, in real life, the first thing that
this part of the protocol would have to deal with is waiting for a message to be given
to it for transmission. However, to simplify things, we will simulate this with a prob-
abilistic delay. Let us assume that a model of the sender looks like[28] :
The Receiving Aspect
The receiving aspect is similar to the sending aspect. It is simplified in so far as
there are no timeouts. Rather than accepting messages for transmission, it simply
pushes the messages up-stream to the higher-level application. Let's look at the
specification[28]: