Deriving protocol specifications from service specifications written in LOTOS

Author

Kant, Christian ; Higashino, Teruo ; Bochmann, Gregor V.

Author_Institution

Dept. d´´ITRO, Montreal Univ., Que., Canada

fYear

1993

fDate

23-26 Mar 1993

Firstpage

310

Lastpage

318

Abstract

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

Keywords

formal specification; open systems; protocols; specification languages; standards; synchronisation; ISO; LOTOS; algorithm correctness; formal service specification; formal specification; protocol specifications; service primitives; service specifications; specification language; standard OSI protocols; synchronization messages; Access protocols; Communication channels; Context; Context-aware services; Delay; Formal specifications; Iron; Service oriented architecture; Specification languages; Standards development;

fLanguage

English

Publisher

ieee

Conference_Titel

Computers and Communications, 1993., Twelfth Annual International Phoenix Conference on

Conference_Location

Tempe, AZ

Print_ISBN

0-7803-0922-7

Type

conf

DOI

10.1109/PCCC.1993.344448

Filename

344448