Analyzing Robustness of UML State Machines

UML State Machines constitute an integral part of software behavior specification within the Unified Modeling Language (UML). The development of realistic software applications often results in complex and distributed models. Hence, potential errors can be very subtle and hard to locate for the developer. In this paper, we present a set of robustness rules that seek to avoid common types of errors by ruling out certain modelling constructs. Furthermore, adherence to these rules can improve model readability and maintainability. The robustness rules constitute a general Statechart style guide for different dialects, such as UML State Machines, Statemate, and Esterel Studio. Based on this style guide, an automated checking framework has been implemented as a plug-in for the prototypical Statechart modeling tool KIEL. Simple structural checks can be formulated in a compact, abstract manner in the Object Constraint Language (OCL). The framework can also incorporate checks that go beyond the expressiveness of OCL by implementing them in Java directly, which can also serve as a gateway to formal verification tools; we have exploited this to incorporate a theorem prover for more advanced checks. As a case study, we adopted the UML well-formedness rules; this confirmed that individual rules can easily be incorporated into the framework.