Achieving high integrity of process control software by graphical design and formal verification

The International Electrotechnical Commission is standardising four compatible languages for designing and implementing programmable logic controllers (PLCs). The language family includes a diagrammatic notation that supports the idea of software ICs to encourage graphical design techniques and systematic software reuse. The authors present an interactive system with a graphical interface for constructing and validating PLC software. The semantics of a graphical design is defined by a mapping associating each design with an executable formal specification. The specification provides the basis for rigorous proofs and early tests of critical properties of a new design. A realistic example illustrates these features