Formal verification of UML-modeled machine controls

Programmable Logic Controllers (PLCs) are applied in a wide field of application and, especially, for safetycritical controls. Thus, there is the demand for high reliability of PLCs. Moreover, the increasing complexity of the PLC programs and the short time-to-market are hard to cope with. Formal verification techniques such as model checking allow for proving whether a PLC program meets its specification. However, the manual formalization of PLC programs is error-prone and time-consuming. This paper presents a novel approach to apply model checking to machine controls. The PLC program is modeled in form of Unified Modeling Language (UML) statecharts that serve as the input to our tool that automatically generates a corresponding formal model for the model checker NuSMV. We evaluate the capabilities of the proposed approach on an industrial machine control