Modelling and formal specification of the real-time manufacturing automation protocol

This paper describes the application of the standard formal description technique Estelle to the modelling and specification of the manufacturing automation protocol three-layer architecture (real-time MAP). The paper discusses the real-time requirements that must be met by communication protocols operating in manufacturing plants, and shows how the Estellle language can be used to specify such protocols formally, including aspects that are crucial in real-time environments, e.g. time constraints, priorities, etc. The formal specification presented here includes the SDA (send data with acknowledgement) service and a deterministic access method for a field bus using token-passing (IEEE 802.4). It has been developed with the Estelle workstation, a set of Estelle-based tools developed in the Esprit Project Sedos Estelle Demonstrator (ESPRIT P1265). The use of Estelle and its associated tools allows not only the formalization of a protocol (uncovering possible ambiguities, logical errors, etc), but also the automatic prototyping, testing, and, eventually, implementation of the protocol. Not less important, the formal specification provides a flexible framework to design new functions, analyze different system configurations or design choices, etc