print · login   

Bounded Retransmission Protocol

Tag: register

Description

The bounded retransmission protocol (BRP) [DKRT97][HSV93] is a variation of the well-known alternating bit protocol [BSW69] that was developed by Philips Research to support infrared communication between a remote control and a television. The bounded retransmission protocol is a data link protocol which uses a stop-and-wait approach known as `positive acknowledgement with retransmission': after transmission of a frame the sender waits for an acknowledgement before sending a new frame. For each received frame the protocol generates an acknowledgement. If, after sending a frame, an acknowledgement fails to appear, the sender times out and retransmits the frame. An alternating bit is used to detect duplicate transmission of a frame. Figure 1 illustrates the operation of our reference implementation of the sender of the BRP. The sender protocol uses the following inputs and outputs:

  • Via an input IREQ(m1,m2,m3), the upper layer requests the sender to transmit a sequence m1 m2 m3 of messages. For simplicity, our reference implementation only allows sequences of three messages, and the only messages allowed are 0 and 1. When the sender is in its initial state INIT, an input IREQ(m1,m2,m3) triggers an output OFRAME(b1,b2,b3,m), otherwise it triggers output ONOK.
  • Via an output OFRAME(b1,b2,b3,m), the sender may transmit a message to the receiver. Here m is the actual transmitted message, b1 is a bit that is 1 iff m is the first message in the sequence, b2 is a bit that is 1 iff m is the last message in the sequence, and b3 is the alternating bit used to distinguish new frames from retransmissions.
  • Via input IACK the receiver acknowledges receipt of a frame and via input ITIMEOUT the sender is informed that a timeout has occurred, due to the loss of either a frame or an acknowledgement message. When the sender is in state WA ("wait for acknowledgement"), an input IACK or ITIMEOUT triggers either an output OFRAME(b1,b2,b3,m) or an output OCONF(i). If the sender is not in state WA, ONOK is triggered.
  • Via an output OCONF(i), the sender informs the upper layer about the way in which a request was handled:
    • i = 0: the request has not been dispatched completely,
    • i = 1: the request has been dispatched successfully,
    • i = 2: the request may or may not have been handled completely; this situation occurs when the last frame is sent but not acknowledged.

An output OCONF occurs when either all three messages have been transmitted successfully, or when a timeout occurs after the maximal number of retransmissions.

Reference implementation of the BRP sender
Fig. 1: Reference implementation of the BRP sender. The input symbols start with I, the output symbols start with O. In addition to symbols, the transitions contain value checks (or guards, ==, <, >) and assignments (=).          

The Mutant Implementations

We consider the following six mutants of the reference implementation of the sender:

Mutant 1
Whereas the reference implementation only accepts a new request in the INIT state, mutant 1 also accepts new requests in state WA. Whenever mutant 1 receives a new request, the previous request is discarded and the sender starts handling the new one.
Mutant 2
Whereas in the reference implementation each message is retransmitted at most 5 times, mutant 2 retransmits at most 4 times.
Mutant 3
Whereas in the reference implementation the alternating bit is only toggled upon receipt of an acknowledgement, mutant 3 also toggles the alternating bit when a timeout occurs.
Mutant 4
In mutant 4 the first and last control bit for the last message are swapped.
Mutant 5
Mutant 5 outputs an OCONF(0) in situations where the reference implementation outputs OCONF(2).
Mutant 6
If the first and the second message are equal then mutant 6 does not transmit the third message, but instead retransmits the first message.

The SUT Models

We used the Uppaal [BDL04] GUI as an editor to create the extended finite state machine (EFSM) in Figure 1 and similar diagrams of the mutant implementations. By means of several Python scripts we automatically generated from an Uppaal .xml file a Java executable that represents the reference and mutant implementations, respectively, as a Java state machine.

Mutant 1 of the reference implementation of the BRP sender
Fig. 2: Mutant 1: Whereas the reference implementation only accepts a new request in the INIT state, mutant 1 also accepts new requests in state WA. Whenever mutant 1 receives a new request, the previous request is discarded and the sender starts handling the new one.          

Mutant 2 of the reference implementation of the BRP sender
Fig. 3: Mutant 2: Whereas in the reference implementation each message is retransmitted at most 5 times, mutant 2 retransmits at most 4 times.          

Mutant 3 of the reference implementation of the BRP sender
Fig. 4: Mutant 3: Whereas in the reference implementation the alternating bit is only toggled upon receipt of an acknowledgement, mutant 3 also toggles the alternating bit when a timeout occurs.          

Mutant 4 of the reference implementation of the BRP sender
Fig. 5: Mutant 4: In mutant 4 the first and last control bit for the last message are swapped.          

Mutant 5 of the reference implementation of the BRP sender
Fig. 6: Mutant 5 outputs an OCONF(0) in situations where the reference implementation outputs OCONF(2).          

Mutant 6 of the reference implementation of the BRP sender
Fig. 7: Mutant 6: If the first and the second message are equal then mutant 6 does not transmit the third message, but instead retransmits the first message.