19-01-2013, 04:41 PM
FINITE STATE MACHINES
FINITE STATE.doc (Size: 154.43 KB / Downloads: 24)
INTRODUCTION
At a low level of abstraction, a protocol is often most easily understood as a state
machine. Design criteria can also easily be expressed in terms of desirable or undesir-
able protocol states and state transitions. In a way, the protocol state symbolizes the
assumptions that each process in the system makes about the others. It defines what
actions a process is allowed to take, which events it expects to happen, and how it will
respond to those events.
The formal model of a communicating finite state machine plays an important role in
three different areas of protocol design: formal validation, protocol synthesis, and
conformance testing. This chapter introduces the main concepts. First the basic finite
state machine model is discussed. There are several, equally valid, ways of extending
this basic model into a model for communicating finite state machines. We select one
of those models and formalize it in a definition of a generalized communicating finite
state machine. The model can readily be applied to represent PROMELA specifications
and to build an automated validator.
There exist many variations of the basic finite state machine model. Rather than list
them all, we conclude this chapter with a discussion of two of the more interesting
examples: the Petri Net and the FIFO Net.
COMMUNICATING FINITE STATE MACHINES
Consider what happens if we allow overlap of the sets of input and output signals of a
finite state machine of the type shown in Table 8.1. In all fairness, we cannot say
what will happen without first considering in more detail what a ‘‘signal’’ is.
We assume that signals have a finite range of possible values and can change value
only at precisely defined moments. The machine executes a two-step algorithm. In
the first step, the input signal values are inspected and an arbitrary executable transi-
tion rule is selected. In the second step, the machine changes its control state in
accordance with that rule and updates its output signals. These two steps are repeated
forever. If no transition rule is executable, the machine will continue cycling through
its two-step algorithm without changing state, until a change in the input signal
values, effected by another finite state machine, makes a transition possible. A signal,
then, has a state, much like a finite state machine. It can be interpreted as a variable
that can only be evaluated or assigned to at precisely defined moments.