This section of the chapter outlines two commonly used methods
for protocol validation based on FSM descriptions of a
protocol.
Looking at a protocol specification, we can identify all the
events that occur and all the states that a protocol entity can
be in. Consider a protocol that operates between two end
points, or processes:
-
First uniquely number events, positively for input (rx/arrival)
and negatively for output (tx/transmission).
-
Second, uniquely number all the states of the protocol, 0, 1, 2, etc.
We can identify sequences of states, simply by starting in each
state, listing
all sequences of possible events, and seeing what the resulting state for
an end point is.
A <#842#> Unilogue<#842#>
is a sequence of states which starts and ends in the same
state, whilst not going through that state in between, e.g.:
0-1-0, 0-1-2-1-0, etc.
A <#843#> Duologue<#843#>
is a pair of these Unilogues for two end points of
a communication.
The <#844#> Duologue Matrix<#844#>
is the set of all possible Duologues (Unilogue pairs).
Protocol Validation is done by designing a function that
operates on the Duologue Matrix, which for each member,
produces values shown in #fnduo1#845>.
#figure846#
Figure: Duologue Matrix Entries
This function can be determined by considering the cases:
-
Post transmission condition
Every case where one end transmits, the other should be in a
receiving state.
-
Deadlock or Pre-reception condition
Every case where the one end is waiting to receive, but the
other does not transmit.
A Duologue is ;SPM_quot;occurable;SPM_quot; if it satisfies these two conditions, and
;SPM_quot;well-behaved;SPM_quot; if all states are reached as well.
Limitations of this method are:
-
All sequences of states must be finite.
-
There can only be two end points of the protocol.
This last point is a very sever drawback in realistic distributed
systems, where there are typically hundreds of end points.