Title :
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
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;
Journal_Title :
Computers, IEEE Transactions on
DOI :
10.1109/TC.1986.1676697
