Formal verification of UML-modeled machine controls

The verification of reliability and functional correctness of the controls of modern machine and manufacturing systems as essential parts of complex industrial automation systems is a time consuming and difficult task. Thus, much effort is spent on automating the verification process by applying formal verification techniques. Formal verification techniques such as model checking allow for proving whether a control system meets its specification. This thesis presents a novel approach to apply model checking to machine controls. The machine control is modeled in form of Unified Modeling Language (UML) statecharts that serve as the input to a tool that automatically generates a corresponding formal model for the model checker NuSMV. The capabilities of the proposed approach are evaluated on an industrial machine control.