Protocol Validation

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:
  1. First uniquely number events, positively for input (rx/arrival) and negatively for output (tx/transmission).
  2. 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>.

Figure: Duologue Matrix Entries

This function can be determined by considering the cases:

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: This last point is a very sever drawback in realistic distributed systems, where there are typically hundreds of end points.