Realistic protocols and the programs that implement them are often quite complicated. Consequently, much research has been done trying to find formal. mathematical techniques for specifying and verifying protocols. In the following sections we will look at some models and techniques. Although we are looking at them in the context of the data link layer, they are also applicable to other layers.
3.5.1 Finite State Machine Models A key concept used in many protocol models is the finite state machine. With this technique, cach protocol machine (ie, sender or receiver) is always in specific state at every instant of time. Its state consists of all the values of its
variables, including the program counter.
In most cases, a large number of states can be grouped for purposes of
analysis. For example, considering the receiver in protocol 3, we could abstract out from all the possible states two important ones: waiting for frame or waiting for frame I. All other states can be thought of as transient just steps on the way to one of the main states. Typically, the states are chosen to be those instants that
the protocol machine is waiting for the next event to happen lie., executing the procedure call wait(event) in our examples) At this point the state of the protocol machine is completely determined by the states of its variables. The number of states is then 2 where n is the number of bits needed to represent all the vari
tables combined. The state of the complete system is the combination of all the states of the two protocol machines and the channel. The state of the channel is determined by its contents. Using protocol 3 again as an example, the channel has four possible States: a 0 frame or a Iframe moving from sender to receiver, an acknowledge
ment frame going the other way, or an empty channel. If we model the sender and receiver as each having two states, the complete system has 16 distinct states A word about the channel state is in order. The concept of a frame being “on the channel” is an abstraction, of course. What we really mean is that a frame has possibly been received, but not yet processed at the destination. A frame remains
“on the channel” until the protocol machine executes From Physical layer and processes it. From each state, there are zero or more possible transitions to other states. Transitions occur when some event happens. For a protocol machine, a transition might occur when a frame is sent, when a frame arrives, when a timer expires.
when an interrupt occurs, etc. For the channel, typical events are insertion of a new frame onto the channel by a protocol machine, delivery of a frame to a proto col machine, or loss of a frame due to noise. Given a complete description of the protocol machines and the channel characteristics, it is possible to draw a directed graph showing all the states as nodes and all the transitions as directed ares.
One particular state is designated as the initial state. This state corresponds to the description of the system when it starts running, or at some convenient starting place shortly thereafter. From the initial state, some, perhaps all of the other states can be reached by a sequence of transitions. Using well-known tech- niques from graph theory (e.g., computing the transitive closure of a graph), it is
possible to determine which states are reachable and which are not. This tech
nique is called reachability analysis (Lin et al., 1987). This analysis can be help ful in determining whether a protocol is correct. Formally, a finite state machine model of a protocol can be regarded as a qua-
druple (S, M. I, T), where: At the beginning of time, all processes are in their initial states. Then events egin to happen, such as frames becoming available for transmission or timers
oing off. Each event may cause one of the processes or the channel to take an iction and switch to a new state. By carefully enumerating each possible succes or to each state, one can build the reachability graph and analyze the protocol Reachability analysis can be used to detect a variety of errors in the protocol
specification. For example, if it is possible for a certain frame to occur in a car in state and the finite state machine does not say what action should be taken, se specification is in error (incompleteness). If there exists a set of states from which no exit can be made and from which no progress can be made (i.e., no
correct frames can be received any more), we have another error (deadlock). A less serious error is protocol specification that tells how to handle an event in a state in which the event cannot occur (extraneous transition). Other errors can also be detected