Composition of service and protocol specifications

One of the most important techniques in protocol design is a compositional technique. Using a compositional technique, a large and complex protocol is designed and verified by combining small and simple protocols which are easy to handle, design and verify. Unlike the other compositional approaches, we propose compositional techniques for simultaneously combining service specifications and protocol specifications based on formal description techniques (FDTs) called LOTOS. The proposed techniques consider alternative, sequential, and interrupt composition of service specifications and protocol specifications. We use the weak bisimulation equivalence (≈), to represent the correctness properties between the service specification and the protocol specification