A LOTOS Specification of the PROWAY Highway Service

The LOTOS language for temporal ordering specification 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 authors present a LOTOS specification of the PROWAY interface for process control applications defined by IEC, the International Electrotechnical Commission. LOTOS is shown to be tailored for the specification of asynchronous systems. In particular, it is suitable for the specification of both the services which define an interface and the protocols which implement it. It is shown 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.