Infrared Remote Control System RC6 Protocol


RC6 protocol is a simplified version of a telecommunication protocol that is used in one of Philips' products. RC6  allows to transmit large blocks of data over unreliable channels within a limited amount of time. After transmission it indicates whether it has been successful. The protocol can find itself in a situation where it does not know whether transmission was a success. In this case it reports accordingly. The key features of the protocol is that data is transmitted in small chunks and only a limited number of retransmissions are allowed for each block of data to be transferred.
 

Description of the external behaviour of the protocol


As for many transmission protocols, the service delivered by RC6 behaves like a buffer, i.e., it reads data from one client to be delivered at another one. There are two features that make the behaviour much more complicated than a simple buffer. Firstly, the input is a large file (that can be modeled as a list), which is delivered in small chunks (packets). Secondly there is a limited amount of time for each packet to be delivered, so we cannot guarantee an eventually successful delivery within the given time bound. It is assumed that either an initial part of the file or the whole file is delivered, so the chunks will not be garbled and their order will not be changed. Both the sender and the receiver obtain an indication whether the whole file has been delivered successfully or not.

The input list l is read from the sending client (producer) on the "input" port. Ideally each packet from the list is delivered on the "output" port, to the receiving client (consumer). Each packet is accompanied by an indication. This indication can be I_FST, I_INC, I_OK, or I_NOK. I_OK is used if the packet is the last element in the list. I_FST is used to indicate that it is first and more will follow. All other packets are accompanied by I_INC. However, when something goes wrong, a "not OK" indication (I_NOK) is delivered without datum. Note that the receiving client does not need a "not OK" indication before delivery of the first chunk nor after delivery of the last one.

The sending client is informed after transmission of the whole file, or when the protocol gives up. An indication is sent out on the "input" port. This indication can be I_OK, I_NOK, or I_DK. After an I_OK or an I_NOK indication, the sender can be sure that the receiver has the corresponding indication. A "don't know" indication I_DK may occur after delivery of last by one packet. (This situation arises, because no realistic implementation can ensure whether the last packet gets lost. The reason is that the information about a successful delivery has to be transported back to somehow over the same unreliable medium. In case the last acknowledgment fails to come, there is no way to know whether the last packet has been delivered or not. After this indication, the protocol is ready to transmit a subsequent file.)
 
 

Description of the protocol


The protocol consists of a sender S equipped with a timer T1, and a receiver R equipped with a timer T2 that exchange data packets via unreliable channels K and L. (See the Figure below). The behaviour of the protocol crucially depends on correct timing.  We first explain the behaviour of the protocol ignoring time, and then we describe how timing has been incorporated in the description and in the model.

   

When channels K and L deliver their data successfully, the protocol behaves as follows. The sender reads the list l to be transmitted from the sending protocol user (producer) and sets the retry counter rn to 0. Then it starts sending the elements of the list on by one. Timer T1 is set and a frame is sent into channel K. This frame consists of three bits and a datum. The first bit indicates whether the datum is the first element of the list. The second bit indicates whether the datum is the last item of the list. The third bit is so-called alternating bit, that is used to guarantee that data is not duplicated. After having sent the frame, the sender waits for an answer (acknowledgment) to arrive from the receiver, or for a timeout. In case an answer arrives, the datum has arrived. After arrival the timer T1 is reset, and depending on whether this was the last element of the list, the sending protocol user is informed of correct transmission, or the next element of the list is sent. It may also be the case that the timer T1 signals a timeout, in which case either the data packet is resent, (after the counter for the number of retries is incremented and the timer is set again), or the transmission of the list is broken off and the receiving side in the protocol is informed accordingly about it. This occurs if the retry counter exceeds the maximum value.

The behaviour of the receiver is simpler. Initially, the receiver waits for a first frame to arrive. The first data packet it receives is delivered at the receiving protocol user (consumer), the receiver starts timer T2. (This timer times out if for a long time nothing is received at the receiver, indicating that transmission of the list has failed.) The receiver also acknowledges the data packet by sending an answer to R via L. Then it simply waits for more packets to arrive. The received packets are always acknowledged, but handled over to the receiving protocol user only if the alternating bit indicates that it is a new one. In this case T2 is reset. Note that (only) if the previous packet was last of the file, then a fresh packet will be the first of the subsequent list and a repeated frame will be still the last of the old list. This goes until T2 times out, which indicates failure of transmission. The receiving client is informed, provided the last element of the file has not just been delivered. Note that if the transmission of the next file starts before T2 expires, the alternating bit scheme is simply continued. This scheme is only interrupted after a failure (indicated by the expiration of T2).

As Promela and Spin cannot model quantitatively time, in our model time and timing constraints are considered as forms of synchronization in the protocol. The synchronization is established using a new set of special signals (and Promela channels), that are not in the original description of the protocol.

Timer T1 times out if an acknowledgment does not arrive "in time" at the sender. It is set when a frame is sent and reset after this frame has been acknowledged. Assuming that the channels K and L deliver data frames in time (if these do not get lost) and assuming that R is always capable of acknowledging an incoming message in bounded time, a late deliver of an acknowledgment can only occur when either channel K or channel L loses a message. One way to describe this is in the model is by making K or L sending a message lost to timer T1, indicating that it may send a timeout. (In other words, we assume that premature timeouts are not possible, i.e., a message must not come after T1 expires.)

Timer T2 is (re)set by the receiver at the arrival of each new frame. It times out if the transmission of a list has been interrupted and it is clear that the sender must have stopped trying to retransmit it. It is also used to model the assumption the sender does not start reading and transmitting a new list before an indication of failure of transmission of the current list has appeared at the receiver -- i.e. the receiver has properly reacted to it. This is necessary because the receiver has not yet switched its alternating bit, so a new frame would be wrongly interpreted as a repetition. In the model we can enforce this assumption by making sender indicating a failure to the receiver by a special rendez-vous channel.

Note that in the model a care should be taken that timers can only signal a time out, if they are set. Resetting a timer turns it off.
 

Assignment

Some hints


Start with small configurations, i.e. with the smallest values for the parameters (e.g., number of chunks and retransmissions). Only after you have gained enough confidence in the correctness of your model try to increase the parameter values. The goal is not to verify a configuration with maximal size, but rather to do it with the limited amount of memory on your machines.

You might also try to minimize the memory requirements using some of the techniques considered during the workshop. For instance, use data types of smaller size (byte instead of int or short), try the minimized automaton option, make some parts atomic, remove sources and sinks, etc.