A compositional approach for constructing communication services and protocols

The complexity of designing communication protocols has lead researchers to develop various techniques for designing and verifying protocols. One of t he most important techniques is a compositional technique. Using a composit ional technique, a large and complex protocol is designed and verified by c omposing small and simple protocols which are easy to handle, design and ve rify. Unlike the other compositional approaches, we propose compositional t echniques for simultaneously composing service specifications and protocol specifications based on Formal Description Techniques (FDTs) called LOTOS. The proposed techniques consider alternative, sequential, interrupt and par allel composition of service specifications and protocol specifications. Th e composite service specification and the composite protocol specification preserve the original behaviour and the correctness properties of individua l service specifications and protocol specifications. We use the weak bisim ulation equivalence (approximate to), to represent the correctness properti es between the service specification and the protocol specification. When a protocol specification is weak bisimulation equivalent to a service specif ication, the protocol satisfies all the logical properties of a communicati on protocol as well as provides the services that are specified in the serv ice specification.