ACHIEVING HIGH INTEGRITY OF PROCESS-CONTROL SOFTWARE BY GRAPHICAL DESIGN AND FORMAL VERIFICATION

The International Electrotechnical Commission is currently 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. This paper presents 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.