Stepwise specification of a sliding-window protocol by means of process algebra

The author introduces a simple language, a subset of the formal language LOTOS, expressive enough to describe a wide range of communication behavior. He shows the applicability of this specification language to a sliding-window protocol taken from the literature. The specifications start with the definition of the service of the protocol. The underlying service is precisely defined, giving the frame into which the protocol has to fit. The first specification defines the protocol entity as a single process. Then this sequential process is decomposed into four parallel processes, taking the replication of data objects into account. In this way, the author obtains a specification that contains adequate detail for use as an implementation specification