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.