Introducing X-machine models to verify PLC ladder diagrams

Ladder diagram is a ubiquitous PLC programming language often used in safety-related control and protection systems. The design and analysis of ladder diagram programs by engineers is often ad hoc using a variety of techniques that may be applied with varying levels of rigour. This paper introduces X-machines, a state-based formalism, to consistently model and verify PLC ladder diagrams. X-machines model control and data flow unambiguously, and have associated with them a test set generation method that is amenable to automation. 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.