Alternating Bit Protocol (NuSMV, w/loops)

Description of the Case Study

We study synthesis-by-scenarios for the Alternating Bit Protocol (ABP), a classic reliable-link protocol that tolerates message loss and duplication by tagging packets/acks with a single alternating bit. The setting contains two components sender and receiver whose actions are abstracted into a single control variable for each model: a_state for a scenario specification and b_state for a synthesized protocol candidate. The goal is scenario conformance: every finite or infinite trace that appears in one of the given scenarios must be simulated by some trace of the synthesized protocol.

We capture conformance via SIMAE (our simulation relation across executions) and a HyperLTL constraint \(\varphi_{\mathrm{conf}}\) of the form \(\forall_{\text{small}}\,\exists_{\text{big}}\), reflecting that scenarios are much smaller than the actual protocol. We consider two synthesized protocols:

• a correct ABP that handles packet loss, and

• an incorrect ABP variant that cannot handle packet loss.

Using HyperQB, our procedure finds a SIMAE witness satisfying \(\varphi_{\mathrm{conf}}\) for the correct ABP, and returns UNSAT for the incorrect one because the packet-loss scenario cannot be simulated by that protocol. The NuSMV model(s) ——————

ABP 1ABP 2ABP 2 buggy

MODULE main
VAR
  a_state : 1..11;

ASSIGN
  init(a_state) := 1;
  next(a_state) :=
    case
      a_state = 1   : 2;
      a_state = 2   : 3;
      a_state = 3   : 4;
      a_state = 4   : 5;
      a_state = 5   : { 6, 7, 8 };
      a_state = 6   : 5;
      a_state = 7   : 5;
      a_state = 8   : 9;
      a_state = 9   : { 10, 11 };
      a_state = 10  : 5;
      a_state = 11  : 1;
      TRUE            : a_state; 
    esac;

The HyperLTL formula(s)

The conformance constraint binds every scenario trace \(\pi_A\) to some protocol trace \(\pi_B\) whose abstract control agrees pointwise according to the scenario–protocol alignment. Intuitively, whenever the scenario is in a control macro-state (e.g., “initial”, “sent”, “ack-processing”), the protocol must be in the corresponding macro-state. We enforce this alignment globally with an invariant.

\[\begin{split}\begin{aligned} \varphi_{\text{conf}} \;=\; \forall \pi_A.\ \exists \pi_B.\ \mathbf{G}\Big( & (a\_state_{\pi_A}{=}1 \leftrightarrow b\_state_{\pi_B}{=}1) \ \land \\ & (a\_state_{\pi_A}{=}2 \leftrightarrow b\_state_{\pi_B}{=}9) \ \land \\ & (a\_state_{\pi_A}{=}3 \leftrightarrow b\_state_{\pi_B}{=}10) \ \land \\ & ((a\_state_{\pi_A}{=}6 \lor a\_state_{\pi_A}{=}7) \leftrightarrow (b\_state_{\pi_B}{=}2 \lor b\_state_{\pi_B}{=}6)) \ \land \\ & (a\_state_{\pi_A}{=}11 \leftrightarrow b\_state_{\pi_B}{=}8) \Big). \end{aligned}\end{split}\]

Formula

Forall A . Exists B . G(((a_state[A] = 1) = (b_state[B] = 1)) & ((a_state[A] = 2) = (b_state[B] = 9)) & ((a_state[A] = 3) = (b_state[B] = 10)) & (((a_state[A] = 6) | (a_state[A] = 7)) = ((b_state[B] = 2) | (b_state[B] = 6))) & ((a_state[A] = 11) = (b_state[B] = 8)))

References

Alur, Rajeev; Martin, Milo; Raghothaman, Mukund; Stergiou, Christos; Tripakis, Stavros; and Udupa, Abhishek. “Synthesizing finite-state protocols from scenarios and requirements.” In Haifa Verification Conference (HVC 2014), pp. 75–91. Springer, 2014.