The statecharts formalism is an extension of conventional finite state machines. Ordinary state transition diagrams are flat, unstructured, and inherently sequential, causing state explosion when modeling systems with parallel threads of control. In statecharts each state consists of a possibly empty hierarchy of statecharts modeling possibly concurrent, communicating state transition diagrams (see Fig. 1).
As in the formalism of Mealy machines, output (events in STATEMATE terminology) can be associated to a transition. Events are the means of communication between parts of a system. Communication is provided by the instantaneous broadcast mechanism. Transition labels in statecharts have the structure Ev[Cond]/Act where Ev is a boolean combination of events, Cond is a boolean condition, and Act is an action. All three parameters are optional. Ev[Cond] is called the trigger part. If the transition source (or sources) is active, Ev occurs and Cond is true then the transition is taken, resulting in the execution of Act, unless there is an enabled transition of higher priority or there is a nondeterministic choice. In the latter case one of the possible transitions is chosen nondeterministically. Events and conditions may refer to the current status of the system. The action part of a transition can generate new events and manipulate variables. Timeout events and scheduling actions are available for the specification of timing aspects. We deal with a sub-dialect where transition labels are restricted as follows:
The operational semantics of statecharts as implemented in STATEMATE is a maximal parallelism semantics inspired by the synchrony hypothesis [1]. This semantics is implicitly defined by that part of the simulation tool that performs stepwise execution of statecharts. The heart of the simulation tool is the basic step algorithm that computes the next possible status ([2]) (or statuses in case of non-determinism) of the SUD.
Next, we illustrate the main ideas underlying this operational semantics by sketching a prefix of a computation of the statecharts given in Figure 1.