The Alternating Bit Protocol (ABP)

The protocol consists of two processes, Sender and Receiver, each having a data buffer and a one-bit state. Sender and Receiver use two channels to communicate with each other, as they do not share any common memory: (a) a data channel from Sender to Receiver for sending bit-packet pairs, and (b) an acknowledgement channel from Receiver to Sender for sending single bits for confirmation. The protocol works as follows:

• Initially, both channels are empty and Sender's bit is different from Receiver's bit.
• Sender repeatedly writes bit-packet pairs < bit, pac > to the data channel, where bit is the Sender's bit and pac is the Sender's data to transmit. If the Sender receives bit from Receiver over the acknowledgement channel, then that is a confirmation that the packet sent has been delivered. In that case, Sender flips its bit and select the next packet to send.
• Receiver writes its bit to the acknowledgement channel repeatedly. When Receiver reads a pair < bit, pac > such that bit is different from its bit, then it stores pac and flips its bit.
• Each of the two communication channels may lose or duplicate messages, at any time, independently of the actions of Sender or Receiver.

A snapshot of the protocol can be found here.

Specification

See abp.maude for the full specification.

Verification

For the ABP we are interested in verifying the following safety property: all messages from Sender are successfully delivered to Receiver, in the correct order, despite the fact that the two communication channels may lose or duplicate messages.

This is achieved in three main steps.

1. ABP ⊢ {inv1, inv2, inv3, inv4}

We prove the following four invariants by simulteneous induction.

• If the data channel contains Senders's bit, then all bits previously sent on the data channel are equal to Senders's bit.

  ceq [inv1]: B' = bit1(S) if C1,< B,P >,C2,< B',P' >,C3 := channel1(S) /\ B = bit1(S)

• If Sender's bit is equal to Receiver's bit, then all bits of the data channel are equal to Senders's bit.

  ceq [inv2]: B = bit1(S) if C1,< B,P >,C2 := channel1(S) /\ bit2(S) = bit1(S)

• If the acknowledgement channel contains Sender's bit, then Receiver's bit is equal to Sender's bit.

  ceq [inv3]: bit2(S) = bit1(S) if D1,B,D2 := channel2(S) /\ B = bit1(S)

• If the acknowledgement channel contains Sender's bit, then all bits previously sent on the acknowledgement channel are equal to Sender's bit.

  ceq [inv4]: B' = bit1(S) if D1,B,D2,B',D3 := channel2(S) /\ B = bit1(S)

See inv.maude for the full proof.

2. ABP + {inv1, inv2, inv3, inv4} ⊢ inv5

We prove another invariant, inv5, using inv1, inv2, inv3 and inv4 as lemmas.

• If acknowledgement channel contains < B, P > such that B is Sender's bit, then P is Sender's current packet.

  ceq [inv5]: P1 = pac(next(S)) if C1,< B,P >,C2 := channel1(S) /\ B1 = bit1(S)

See inv5.maude for the full proof.

3. ABP + {inv2, inv3, inv5} ⊢ {goal1, goal2}

The safety property of interest is formalized as the conjunction of two goals.

• If Sender's bit is equal to Receiver's bit, then all packets sent have been delivered.

  ceq [goal1]: mk(next(S:Sys)) = list(S:Sys) if bit2(S:Sys) = bit1(S:Sys)

• If Sender's bit is different from Receiver's bit, then the last packet sent has not been delivered.

  ceq [goal2]: mk(next(S:Sys)) = pac(next(S:Sys)),list(S:Sys) if not bit2(S:Sys) = bit1(S:Sys)

See goal.maude for the full proof.