Composition of service specifications

Gurdip Singh, Ionut Buricea, Zhenyu Mao

Research output: Chapter in Book/Entry/PoemConference contribution

4 Scopus citations


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).

Original languageEnglish (US)
Title of host publicationInternational Conference on Network Protocols
PublisherIEEE Computer Society
Number of pages9
StatePublished - 1998
Externally publishedYes
EventProceedings of the 1998 International Conference on Network Protocols, ICNP - Austin, TX, USA
Duration: Oct 13 1998Oct 16 1998


OtherProceedings of the 1998 International Conference on Network Protocols, ICNP
CityAustin, TX, USA

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Composition of service specifications'. Together they form a unique fingerprint.

Cite this