Refinement Patterns for Hierarchical UML State Machines

While the semantics of (labeled) transition systems and the relations between these are well understood, the same still needs to be achieved for UML 2.x state machines, because the UML standard is ambiguous and admits many semantics, which are often defined in terms of labeled transition system us. A formal semantics for UML state machines with interlevel transitions and notions of refinement are described to enable the study of transformations, i.e., functions from state machines to state machines, and to establish the conditions under which these transformations are refinement steps. Many of these transformations are described and shown to he refinement steps. A language extension is finally proposed that help modelers to ensure that all transformations are indeed refinements.