DERIVING PROTOCOL SPECIFICATIONS FROM SERVICE SPECIFICATIONS WRITTEN IN LOTOS

A complete communication system is broken down into a number of protoc ol layers each of which provides services to the layer above it and us es services provided by its underlying layer. A service specification defines a particular ordering of the operations that a given layer pro vides to the layer above it. The active elements in each layer are cal led entities and they use a protocol in order to implement their servi ce definition. On the basis of this relation between the service and p rotocol concepts we have developed algorithms for deriving protocol en tity specifications from a formal service specification. The derived p rotocol entities ensure the correct ordering of the service primitives by exchanging synchronization messages through an underlying communic ation medium. This paper presents an extended version of our earlier d erivation algorithms. This version of the algorithm can handle all ope rators and unrestricted process invocation and recursion as defined by basis LOTOS. The correctness of this derivation algorithm is formally proved.