JUCS - Journal of Universal Computer Science 9(2): 138-151, doi: 10.3217/jucs-009-02-0138
A Case Study in Verification of UML Statecharts: the PROFIsafe Protocol
expand article infoRobi Malik‡, Reinhard Mühlfeld§
‡ Department of Computer Science, University of Waikato Hamilton,, New Zealand§ Siemens Corporate Technology, Erlangen, Germany

Corresponding author: Robi Malik ( robi@cs.waikato.ac.nz )

© Robi Malik, Reinhard Mühlfeld.
This article is freely available under the J.UCS Open Content License.
Citation: Malik R, Mühlfeld R (2003) A Case Study in Verification of UML Statecharts: the PROFIsafe Protocol. JUCS - Journal of Universal Computer Science 9(2): 138-151. https://doi.org/10.3217/jucs-009-02-0138
Open Access
Abstract
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 denite-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 denite-state machines, and points out important aspects and problems occurring during the modelling and verification of industrial applications.
Keywords
reliability, verification