An open software architecture for the verification of industrial controllers

The paper presents a tool architecture which supports the formal verification of logic controllers for processing systems. The tool's main intention is to provide a front-end for modelling the controller as well as the processing systems. The models are automatically transformed into representations which can be analysed by existing model checking algorithms. While the first part of the paper gives an overview of the complete architecture, the second part introduces a newly developed modelling interface: Process Control Event Diagrams (PCEDs) are formally defined as a suitable means to represent the flow of information in controlled processes. The transformation of PCEDs into verifiable code is described, and the whole procedure of modelling, model transformation and verification is illustrated with a simple processing system.