Protocol Example 1

Protocol Example: Verification Using Discrete-Event Systems


• Description



• We consider the problem of reliably transmitting frames of data over an unreliable channel. The goal of a protocol for the problem is to ensure that a sender gets data from a host computer, passes that data over a communication channel to a reciever, which must then pass the data to another host in the same order and without duplicates as the data sequence received by the sender from the originating host. Finite-state machine translations, labeled SNDR and RCVR, of the protocol for the sender and receiver, as well as for the communication channel, labeled CHNL, are provided in the figure below.

• In the figure, getframe means the sender gets a new frame from the source host; send0 means the sender sends the most recent frame it got to the reciever with a sequence number of 0; rcv0 means the reciever recieves a frame whose sequence number is 0; sendack means the reciever sends an acknowledgement to the sender; rcvack means the sender reiceves an acknowledgement from the reciever; passtohost means the receiver passes the frame it just recieved to the target host; timer means the sender starts the timer; timeout means the timer times out; cksumerr means that a frame has arrived damaged; cksumerrack means that an acknowledgement has arrived damaged; and lose means the channel loses the message in it. The set of all possible events is represented by Σ.



• Modeling Plant



• The plant under investigation, called G, is given by the parallel composition of the three machines from above, and is a machine consisting of 56 states, as can be seen in the figure below.

• Protocol Verification



• The successful protocol must possess the following property: at any point in time, the sequence of data passed by the receiver to the target host must be a prefix of the sequence gotten by the sender from the source host. This is called a safety property.

• To describe the safety property, we define the language E = L(G)∩LEGAL, where LEGAL is generated by the finite-state machine above. The requirement in LEGAL that getframe and passtohost strictly alternate ensures that if new data is passed to the target host, it is passed in the correct order and without duplicates. This means sequences of events that are contained in LEGAL satisfy the safety property.



• In order to systematically verify whether the protocol satisfies the intended safety requirement, we can compute infCCCo(E) (see the referenced publication for details). We see that infCCCo(E) ≠ E. We know that all the strings in infCCCo(E) - E are sequences of events in which the protocol fails but which resemble successful runs of the protocol, meaning that the sender cannot distinguish between some sequences. This means E is not co-observable with respect to the plant G.



• For more information on this example:

K. Rudie and W.M. Wonham, "Protocol Verification Using Discrete-Event Systems", in Proceedings of the IEEE Conference on Decision and Control (CDC) , Tucson, AZ, pp. 3770-3777, 1992.

Back to Protocol Examples