Re-engineering approach for PLC programs based on formal methods

Today there is a standard for the implementation of programs on Programmable Logic Controllers (PLCs). Furthermore there are methods for the formal development of these programs. The standard allows the interchange of algorithms (e. g. if a new hardware should be used) and the formal methods allow the rigid proof of functionality especially needed in safety critical applications (e. g. using model checking). However, there are a lot of existing PLC programs that have been implemented in proprietary languages before a standard existed and even today formal methods are scarcely used during design. This work outlines a re-engineering approach based on the formalization of PLC programs. The PLC program modules are modeled as Finite State Machines (FSMs). These FSMs are able to communicate with each other to describe the complete dynamic of the PLC system. The resulting formal model can serve as a basis for editing and analyzing the system. The transformation of PLC programs into a vendor independent format and the visualization of its structure is identified as an important intermediate step in this process. It is shown how XML and corresponding technologies can be used for the formalization, visualization, re-implementation, and software measurement of existing PLC programs.