Introducing X-machine models to verify PLC ladder diagrams

Ladder diagram is a ubiquitous PLC programming language often used in safet y-related control and protection systems. The design and analysis of ladder diagram programs by engineers is often ad hoc using a variety of technique s that may be applied with varying levels of rigour. This paper introduces X-machines, a state-based formalism, to consistently model and verify PLC l adder diagrams. X-machines model control and data flow unambiguously, and h ave associated with them a test set generation method that is amenable to a utomation. This work shows by an example, namely an oil tank warning system , how ladder diagram programs, can be successfully modelled using variants of the X-machine model. Crown Copyright (C) 2001 Published by Elsevier Scie nce B.V. All rights reserved.