A case study in verification of UML statecharts: the PROFIsafe protocol

We discuss our experience obtained during the PROFIsafe verification and test case generation project at Siemens Corporate Technology. In this project, a formal analysis of the PROFIsafe protocol for failsafe communication has been carried out. A formal model based on finite-state machines has been obtained from the UML specification of the protocol. This model has been analysed with formal verification techniques, and several important properties have been proven. Based on the verified model, a set of test cases for the automatic execution of conformance tests has been derived. The paper explains how the UML statecharts defining the PROFIsafe protocol are translated into finite-state machines, and points out important aspects and problems occurring during the modelling and verification of industrial applications