Equivalence transformations on statecharts

Statecharts are a popular representation technique for conceptual models of the dynamics of a universe of dis-course. However, designers are not supported in their work with dynamic models as well as they are for working with static models. We present a meta-model and a formalization of the semantics of a statechart language. Important re-sults are the definition of the equivalence of statecharts and a sound and complete axiomatization of the equivalence. Based on this we define a set of basic schema transforma-tions which do not change the semantics of a model. These transformations can be used to successively transform stat-echarts to achieve design goals or to prepare them for im-plementation. 1