In: CONCUR'97, pages 181-195. July 1997.
Abstract: In this paper we present an algebraic approach to statecharts as they are used in the STATEMATE tool in the style of ``Petri-Nets are Monoids'' for place-transition nets developed by Meseguer and Montanari. We apply the framework of high-level-replacement systems, a categorical generalization of graph transformation systems, in order to define union as horizontal as well as transformation and refinement as vertical structuring techniques for statecharts. The first main result shows compatibility of union and transformation in a suitable category of statecharts. We present an algorithm for the computation of all transitions enabled within one step. The second main result shows the correctness of this algorithm. We define refinement morphisms for statecharts, which allow refinement of arbitrary states, in contrast to concepts in the literature where only basic and root states are subject of refinement. The third main result shows that refinement morphisms are compatible with the behavior of statecharts as defined in the formal semantics.
Keywords: statecharts; structuring techniques; high-level-replacement systems.