A Formal Method Based Re-Implementation Concept for PLC Programs and Its Application

Programmable logic controllers (PLCs) are still the workhorse of industrial automation. The programming and adaptation of the software for PLCs - i.e. the implementation of the control algorithms - are expensive and cumbersome tasks. Today the re-implementation of an existing PLC program on a new platform, as it is supported by industrial tools on a low level, requires considerable manual re-working by a specialist. Known re-implementation processes do not allow a fully automatic transfer to a new platform. Furthermore they lack re-documentation of the code which makes it hard to understand and to follow the implemented algorithms. To avoid these problems, this paper proposes a re-implementation concept for existing PLC programs based on formal methods. An application of this concept to a lab system is presented to assess its applicability