Tag: register
The alternating bit protocol (ABP) is a simple communication protocol for reliable transmission of messages (frames) [BSW69], and a standard benchmark example in formal methods research. The protocol can be used in a setting in which two agents, a sender and a receiver, communicate via two lossy channels: a channel M for messages from sender to receiver and channel A for acknowledgements from receiver to sender, see Figure 1.
The ABP guarantees reliable transmission by retransmitting lost or corrupted messages, and also ensures that the order of messages is preserved. Each message the sender transmits contains a data part and an additional bit, i.e., a value that is 0 or 1. After transmission, the sender waits for an acknowledgement from the receiver (with the same bit) via A. If no correct acknowledgement arrives, the sender retransmits the message with the same bit. Otherwise, the sender flips the bit and starts transmitting the next message.