Deriving protocol specifications from service specifications written in LOTOS

Based on the relation between the service and protocol concepts the authors have developed algorithms for deriving protocol entity specifications from a formal service specification. The derived protocol entities ensure the correct ordering of the service primitives by exchanging synchronization messages through an underlying communication medium. A new version of the algorithms is proposed. It is an extension of the method to a more comprehensive specification language. This version of the algorithm can handle all operators and unrestricted process invocation and recursion as defined by basic LOTOS. LOTOS is a language which has been developed within ISO for the formal specification of standard OSI protocols and services. The correctness of the algorithm is formally proved