Communicating Finite State Machines

Finite State Machines (FSMs) are an attractive model for embedded systems. The amount of memory required by such a model is always decidable, and is often an explicit part of its specification. Halting and performance questions are always decidable since each state can, in theory, be examined in finite time. In practice, however, this may be prohibitively expensive. A traditional FSM consists of:
_ a set of input symbols (the Cartesian product of the sets of values of the input signals),
_ a set of output signals (the Cartesian product of the sets of values of the output signals),
_ a finite set of states with a distinguished initial state,
_ an output function mapping inputs and states to outputs, and
_ a next-state function mapping inputs and states to (next) states.
The input to such a machine is a sequence of input symbols, and the output is a sequence of output symbols.
Traditional FSMs are good for modeling sequential behavior, but are impractical for modeling concurrency or memory because of the so-called state explosion problem. A single machine mimicking the concurrent execution of a group of machines has a number of states equal to the product of the number of states of each machine. A memory has as many states as the number of values that can be stored at each location raised to the power of the number of locations. The number of states alone is not always a good indication of complexity, but it often has a strong correlation. Harel advocated the use of three major mechanisms that reduce the size (and hence the visual complexity) of finite automata for modeling practical systems [15]. The first one is hierarchy, in which a state can represent an enclosed state machine.
That is, being in a particular state a has the interpretation that the state machine enclosed by a is active. Equivalently, being in state a means that the machine is in one of the states enclosed by
a. Under the latter interpretation, the states of a are called “or states.” Or states can exponentially reduce the complexity (the number of states) required to represent a system. They compactly describe the notion of preemption (a high-priority event suspending or “killing” a lower priority task), that is fundamental in embedded control applications. The second mechanism is concurrency. Two or more state machines are viewed as being simultaneously active. Since the system is in one state of each parallel state machine simultaneously, these are sometimes called “and states.” They also provide
a potential exponential reduction in the size of the system representation.
The third mechanism is non-determinism. While often nondeterminism is simply the result of an imprecise (maybe erroneous) specification, it can be an extremely powerful mechanism to reduce the complexity of a system model by abstraction.
This abstraction can either be due to the fact that the exact functionality must still be defined, or that it is irrelevant to the properties currently considered of interest. E.g., during verification of a given system component, other components can be modeled as non-deterministic entities to compactly constrain the overall behavior. A system component can also be described non-deterministically to permit some optimization during the implementation phase. Non-determinism can also provide an exponential reduction in complexity. These three mechanisms have been shown in [16] to cooperate
synergistically and orthogonally, to provide a potential triple exponential reduction in the size of the representation with respect to a single, flat deterministic FSM6. Harel’s Statecharts model uses a synchronous concurrency model (also called synchronous composition). The set of tags is a totally ordered countable set that denotes a global “clock” for the system. The events on signals are either produced by state tran sitions or inputs. Events at a tick of the clock can trigger state transitions in other parallel state machines at the same clock. Unfortunately, Harel left open some questions about the
semantics of causality loops and chains of instantaneous (same tick) events, triggering a flurry of activity in the community that has resulted in at least twenty variants of Statecharts [17]. Most of these twenty variants use the synchronous concurrency model. However, for many applications, the tight coordination implied by the synchronous model is inappropriate. In response to this, a number of more loosely coupled asynchronous FSM models have evolved, including behavioral FSMs [18], SDL process networks [18], and codesign FSMs [19].
A model that is closely related to FSMs is Finite Automata. FAs emphasize the acceptance or rejection of a sequence of inputs rather than the sequence of output symbols produced in response to a sequence of input symbols. Most notions, such as composition and so on, can be naturally extended from one model to the other. In fact, any of the concurrency models described in this paper can be usefully combined with FSMs. In the Ptolemy project [14], FSMs are hierarchically nested with dataflow, discrete-event, or synchronous/reactive models [20]. The nesting is arbitrarily deep and can mix concurrency models at different levels of the hierarchy. This very flexible model is called “*charts,” pronounced “star charts,” where the asterisk is meant to suggest a wildcard. Control Flow Expressions (CFEs, [21]) have been recently proposed to represent the control flow of a set of operations in a cycle-based specification language. CFEs are an algebraic model extending Regular Expressions [9] and can be compiled into FSMs that can be used in the synthesis of a control unit.
B.3 Synchronous/Reactive
In a synchronous model of computation, all events are synchronous, i.e., all signals have events with identical tags. The tags are totally ordered, and globally available. Simultaneous events (those in the same clock tick) may be totally ordered, partially ordered, or unordered, depending on the model of computation. Unlike the discrete-event model, all signals have events at all clock ticks, simplifying the simulator by requiring no sorting. Simulators that exploit this simplification are called cyclebased or cycle-driven simulators. Processing all events at a given clock tick constitutes a cycle. Within a cycle, the order in which events are processed may be determined by data precedences, which define microsteps. These precedences are not allowed to be cyclic, and typically impose a partial order (leaving some arbitrary ordering decisions to the scheduler). Cyclebased models are excellent for clocked synchronous circuits, and have also been applied successfully at the system level in certain signal processing applications.
A cycle-based model is inefficient for modeling systems where events do not occur at the same rate in all signals. While conceptually such systems can be modeled (using, for example, special tokens to indicate the absence of an event), the cost of processing such tokens is considerable. Fortunately, the cyclebased model is easily generalized to multirate systems. In this case, every nth event in one signal aligns with the events in another. A multirate cycle-based model is still somewhat limited. It is an excellent model for synchronous signal processing systems where sample rates are related by constant rationalmultiples, but in situations where the alignment of events in different signals is irregular, it can be inefficient. The more general synchronous/reactive model is embodied
in the so-called synchronous languages [22]. Esterel [23] is a textual imperative language with sequential and concurrent statements that describe hierarchically-arranged processes. Lustre [24] is a textual declarative language with a dataflow flavor and a mechanism for multirate clocking. Signal [25] is a textual relational language, also with a dataflow flavor and a more powerful clocking system. Argos [26], a derivative of Harel’s Statecharts [27], is a graphical language for describing hierarchical finite state machines. Halbwachs [5] gives a good summary of this group of languages.
The synchronous/reactive languages describe systems as a set of concurrently-executing synchronized modules. These modules communicate through signals that are either present or absent in each clock tick. The presence of a signal is called an event, and often carries a value, such as an integer. The modules are reactive in the sense that they only perform computation and produce output events in instants with at least one input event. Every signal in these languages is conceptually (or explicitly) accompanied by a clock signal, which has meaning relative to other clock signals and defines the global ordering of events. Thus, when comparing two signals, the associated clock signals indicate which events are simultaneous and which precede or follow others. In the case of Signal and Lustre, clocks have complex interrelationships, and a clock calculus allows a compiler to reason about these ordering relationships and to detect inconsistencies in the definition. Esterel and Argos have simpler clocking schemes and focus instead on finite-state control. Most of these languages are static in the sense that they cannot request additional storage nor create additional processes while running. This makes them well-suited for bounded and speedcritical embedded applications, since their behavior can be extensively
analyzed at compile time.
This static property makes a synchronous program finite-state, greatly facilitating formal
verification. Verifying that a synchronous program is causal (noncontradictory and deterministic) is a fundamental challenge with these languages. Since computation in these languages is delayfree and arbitrary interconnection of processes is possible, it is possible to specify a program that has either no interpretation (a contradiction where there is no consistent value for some signal) or multiple interpretations (some signal has more than one consistent value). Both situations are undesirable, and usually indicate a design error. A conservative approach that checks for causality problems structurally flags an unacceptably large number of programs as incorrect because most will manifest themselves only in unreachable program states. The alternative, to check for a causality problem in any reachable state, can be expensive since it requires an exhaustive check of the state space of the program. In addition to the ability to translate these languages into finite-state descriptions, it is possible to compile these languages directly into hardware. Techniques for translating both Esterel [28] and Lustre [29] into hardware have been proposed. The result is a logic network consisting of gates and flip-flops that can be optimized using traditional logic synthesis tools.
To execute such a system in software, the resulting network is simply simulated. The technique is also the basis to perform more efficiently causality checks, by means of implicit state space traversal techniques [30].