A LOTOS Specification of the PROWAY Highway Service

Author

Carchiolo, Vincenza ; Faro, Alberto ; Mirabella, Orazio ; Pappalardo, Giuseppe ; Scollo, Giuseppe

Author_Institution

Institute of Information and Telecommunications, Faculty of Engineering, University of Catania

Issue

11

fYear

1986

Firstpage

949

Lastpage

968

Abstract

The Language for temporal ordering specification (LOTOS) is a formal description technique whose development is under way within ISO, the International Organization for standardization, mainly for application to open systems interconnection (OSI) standards. The paper presents a LOTOS specification of the PROWAY interface for process control applicatioins, defined by IEC, the International Electrotechnical Commision. LOTOS is shown to be tailored for the specification of asynchronous systems. In particular, it proves suitable for the specification both of the services which define an interface and of the protocols which implement it. The paper shows how LOTOS supports formal reasoning aimed at establishing consistency between service and protocol specifications. Two examples of such a verification are developed that are related to the PROWAY interface. Finally, advantages and limitations of this approach are outlined.

Keywords

Computer communication standards; formal specifications; local area networks; multicast communication services; process control; protocol verification; rapid prototyping; temporal ordering; Communication standards; Formal specifications; IEC; Logic; Mathematical model; Open systems; Process control; Protocols; Road transportation; Standardization; Computer communication standards; formal specifications; local area networks; multicast communication services; process control; protocol verification; rapid prototyping; temporal ordering;

fLanguage

English

Journal_Title

Computers, IEEE Transactions on

Publisher

ieee

ISSN

0018-9340

Type

jour

DOI

10.1109/TC.1986.1676697

Filename

1676697