Deriving protocol specifications from service specifications written in LOTOS |
| |
Authors: | Christian Kant Teruo Higashino Gregor von Bochmann |
| |
Affiliation: | (1) Département d’IRO, Université de Montréal, C.P. 6128, Succursale A, Montréal, Québec, H3C 3J7, Canada, CA |
| |
Abstract: | Summary. A complete communication system is broken down into a number of protocol layers each of which provides services to the layer
above it and uses services provided by its underlying layer. A service specification defines a particular ordering of the
operations that a given layer provides to the layer above it. The active elements in each layer are called entities and they
use a protocol in order to implement their service definition. On the basis of this relation between the service and protocol
concepts we 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. This paper presents an extended version of our earlier derivation algorithms. This version
of the algorithm can handle all operators and unrestricted process invocation and recursion as defined by basis LOTOS. The
correctness of this derivation algorithm is formally proved.
Received: January 1992 / Accepted: February 1996 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|