Composition of service specifications

The service specification ss(P) of a protocol P defines the services provided by the protocol and its protocol specification ps(P) specifies the rules of message exchange to ensure the service. Protocol composition has been advocated as an attractive way to design complex protocols. Several techniques have been studied for composition of protocol specifications. In these techniques, to combine component protocols P and Q to design R, ps(P) and ps(Q) are first combined to obtain ps(R) and then inference rules are used to derive ss(R). In this paper, we explore an alternative strategy in which we allow composition to be specified at the service specification level (that is, ss(P) and ss(Q) are first combined to obtain ss(R)). Given ss(R), we provide an algorithm to mechanically combine ps(P) and ps(Q) to generate ps(R) such that ps(R) satisfies ss(R). We show that analysis of ss(R) is sufficient to ensure that ps(R) satisfies certain safety and liveness properties. This results in efficient validation as state space of ss(R) is typically significantly smaller than that of ps(R).