Issue No.11 - November (1986 vol.35)
V. Carchiolo , Institute of Information and Telecommunications, Faculty of Engineering, University of Catania
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.
temporal ordering, Computer communication standards, formal specifications, local area networks, multicast communication services, process control, protocol verification, rapid prototyping
V. Carchiolo, A. Faro, O. Mirabella, G. Pappalardo, G. Scollo, "A LOTOS Specification of the PROWAY Highway Service", IEEE Transactions on Computers, vol.35, no. 11, pp. 949-968, November 1986, doi:10.1109/TC.1986.1676697