A re-engineering approach for PLC programs using finite automata and UML

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 prove of functionality especially needed in safety critical applications (e.g. using model checking). However, there is 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. This paper outlines an approach to formalize existing PLC programs implemented in the widely used STEP5 language. It consists of two steps: first the modular structure of the program is transferred to a UML model and in a second step the algorithms contained in the modules are converted to finite automata. This conversion uses an abstraction method to avoid large automata.