JUCS - Journal of Universal Computer Science 7(1): 37-53, doi: 10.3217/jucs-007-01-0037
An Open Software Architecture for the Verification of Industrial Controllers
expand article infoHeinz Treseler‡, Olaf Stursberg‡, Paul W. H. Chung§, Shuanghua Yang§
‡ University of Dortmund, Dortmund, Germany§ Loughborough University, United Kingdom

Corresponding author: Heinz Treseler ( h.treseler@ct.uni-dortmund.de )

© Heinz Treseler, Olaf Stursberg, Paul W. H. Chung, Shuanghua Yang.
This article is freely available under the J.UCS Open Content License.
Citation: Treseler H, Stursberg O, Chung PWH, Yang S (2001) An Open Software Architecture for the Verification of Industrial Controllers. JUCS - Journal of Universal Computer Science 7(1): 37-53. https://doi.org/10.3217/jucs-007-01-0037
Open Access
Abstract
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.
Keywords
model checking, formal verification, logic controller, process control event diagram, tool development