On the Formal Semantics of VisualSTATE Statecharts

This paper presents a formal semantics of statecharts - a visual language successfully employed in design of control algorithms. Our formalization is implementation oriented, with efficiency in the focus. It has been used as a specification in development of SCOPE, an experimental code generator for embedded systems.

The version of statecharts we describe is that implemented in commercial development tool IAR VisualSTATE. IAR visualSTATE statecharts are similar to Harel's original statecharts, with several additions and some restrictions. They mostly agree with UML state diagrams on syntax and semantics. A small survey is appended comparing visualSTATE statecharts terminology and concepts with those of D.Harel's original statecharts and UML statechart diagrams. The paper may be perceived as a formal equivalent to the official Concept Guide delivered with the VisualSTATE software package from IAR.