TReX's Examples

The Alternating Bit Protocol

Description of the example

The Alternating Bit Protocol is a reliable transport protocol of stop-and-wait family. It uses positive acknowledgement (ACK) and additional information of one bit to each message exchanged. The additional bit is used to identify a message in the sequence of messages sent. Only one bit suffices because no new data message is sent before the acknowledgement for the previous data message sent is not arrived (stop-and-wait).

The model we consider for this protocol is build from two automata (for sender and receiver) which exchange messages through two fifo lossy channels M (for messages sent from sender to receiver) and A (for acknowledgements sent from receiver to sender). The sender reads each message of the producer and sends it through M to the receiver with its additional bit. Then, it waits for an acknowledgement of this message (with the same bit) through A. If the acknowledgement does not arrive, the sender resends the message (with the same bit). When it receives the acknowledgement, the sender sends the next message read from the producer with an incremented bit.

In our model, the channels M and A are unbounded because the resent of data or acknowledgement messages is not bounded (see states s1, s3, r0, r2 in automata below). The following figures give the automata of the sender and receiver. In these automata, M!m0 means the sending of a message of data with bit 0 through channel M, M?m0 means the reception of data message with bit 0 through M, and nop means that the transition has no effect on channels.

The symbolic graph obtained is abp.aut. After reduction of internal actions (sending and receiving through unreliable channels) by weak-bisimulation, we obtain the graph below which corresponds to a reliable transport of data between producer and consumer.