Towards a Formal Operational Semantics of UML Statechart Diagrams

Abstract

Statechart Diagrams are a notation for describing behaviours in the framework of UML, the Unified Modeling Language of objectoriented systems. UML is a semiformal language, with a precisely defined syntax and static semantics but with an only informally specified dynamic semantics. UMLStatechart Diagrams differ fromclassical statecharts, as defined by Harel, for which formalizations and results are available in the literature. This paper sets the basis for the development of a formal semantics for UML Statechart Diagrams based on Kripke structures. This forms the first step towards model checking of UML Statechart Diagrams. We follow the approach proposed by Mikk and others: we first map Statechart Diagrams to the intermediate format of extended hierarchical automata and then we define an operational semantics for these automata. We prove a number of properties of such semantics which reflect the design choices of UML Statechart Diagrams.