Bus communication protocol for remote reading and writing: Formal specification and verification

In the context of computer-integrated manufacturing, communication protocols are being developed for remote sensor reading and remote actuator writing. A formal description technique that is used to specify a fieldbus protocol is introduced. This protocol is based on message broadcasting and control centralized via a mean station. Medium access and data-link control layers are the important features. The architectural principles and the distributed behavior of system modules are depicted by means of labeled Petri nets. These executable specifications are used to perform a formal analysis of components and allow properties of the interconnected system to be verified