Statecharts and synchronous languages:

Statecharts [38] represents an improved version of the structured methods. A graphic tool called ``Statemate'' [41] exists to implement the formalism. Methods similar to that of Statecharts may be found in [29].

In Statecharts, the normal state transition diagram is enhanced with hierarchical and compositional features. For example, states can be clustered into super-states with the possibility of ``zooming in'' and ``zooming out'' of states. In AND decomposition, states are split into orthogonal (concurrent) subcomponents that communicate via broadcasting. OR decomposition decomposes a state into sub-states such that control resides in exactly one sub-state.

Statemate is formally based on a precisely defined (although rather complex) semantics. As an important consequence, there is an automated simulation tool which allows the user to execute the model. Exhaustive checking of all possible behaviours (for small systems) is supported. Models (e.g. of the controller) can be compiled into a target environment, although this tool is not yet fully developed. Formal verification is not yet supported, nor are time constraints treated in sufficient detail.

According to [86], the real-time aspects of Statecharts semantics is underdeveloped. A notation is needed for periodic timing functions, and for the specification of timing exceptions without the need to introduce additional states.

Recently, some progress has been made in providing formal analysis techniques for Statecharts. A fully abstract compositional semantics of Statecharts has been presented [53].

The simplest kind of semantics uses the operational notion of the set of all observable behaviours of a program or system. A behaviour may be defined as an infinite sequence of states that the system computes in one run. Such an operational semantics cannot usually be used to deliver a compositional (modular) semantics. In a compositional semantics, a compound system M1| M2 is described in terms of the semantics of the component systems M1 and M2. A fully abstract semantics defines the behaviour of the system in sufficient detail without violating the principle of compositionality, i.e. such a semantics does not distinguish between more systems than is necessary to provide a compositional semantics.

The importance of compositionality is that structured program verification can be undertaken. Components of the system can be checked independently, and then combined to provide a verifiably correct compound program.

In addition to the abstract semantics of Statecharts presented in [53], there is an alternative version of Statecraft semantics. In [119], a semantics is presented that uses micro and macro-steps. Observable macro-steps are decomposed into a number of micro-steps. If event A triggers B then these events occur in subsequent micro-steps within the same macro-step. Thus a chain of causality inside one macro-step is modelled by a sequence of micro-steps. This avoids some of the causal paradoxes that occur in synchronous languages such as Statecharts.

The ``synchrony hypothesis'' assumes that a program instantly reacts to external events. In practice this means that the reaction time of the controller is always shorter than the minimum delay separating two successive external events in the plant. In addition to Statecharts, the languages Esterel [11], Signal [9] and Lustre [16] have been designed with the synchrony hypothesis in mind. The synchrony hypothesis must be applied with care as it can lead to causal paradoxes such as events disabling their own cause. This hypothesis is not always realistic, as the plant usually involves spontaneous behaviour that may occur at any moment of time. Languages such as Esterel do not allow for nondeterminism which is also not realistic for representing plants.