Semantic Issues in UML 2.0 State Machines
A precise semantics for the modeling language UML 2.0 is necessary for code generation and for formal verification of models during the early stages of design. We present a formal semantics of the firing of transitions in UML 2.0 state machines. In particular, we handle shallow/deep history pseudostates, final states, join/fork pseudostates, entry/exit actions and the different kinds of transition. Furthermore, our semantics captures all orderings of actions in a run-to-completion step. We point out ambiguities and uncertainties in the UML 2.0 standard, especially in the meaning of history pseudostates and priority between transitions. We discuss different attempts in resolving these.