Correctness of Alternating Bit Protocol

Correctness of the Alternating Bit Protocol

The specification and proof score for this example are given in section 1, and the output in section 2. The diagram below suggests the level of detail of the protocol model that we specify and verify. The specification is rather sophisticated (e.g., the way that fairness of transmission errors is handled), and the justifications and explanations that go with this example are much more elaborate than in previous examples. For these, the interested reader should consult the paper A Hidden Proof of the Alternating Bit Protocol. This example was done by Kai Lin and Joseph Goguen.


1. BOBJ Source Code

*** file: /tatami/bobj/examples/abp/abp.bob *** correctness of alternating bit protocol bth STREAM is sort DataStream . pr NAT . op hd_ : DataStream -> Nat . op tl_ : DataStream -> DataStream . op _&_ : Nat DataStream -> DataStream . var N : Nat . var Is : DataStream . eq hd(N & Is) = N . eq tl(N & Is) = Is . eq hd Is & tl Is = Is . *** lemma end bth FAIR-STREAM is pr STREAM *(sort DataStream to FairStream). dsort Mark . ops ok err : -> Mark . op eq : Mark Mark -> Bool [comm] . var M : Mark . eq eq(M, M) = true . eq eq(err, ok) = false . op fhd_ : FairStream -> Mark . op ftl_ : FairStream -> FairStream . var N : Nat . var F : FairStream . eq fhd(0 & F) = ok . eq ftl(0 & F) = F . eq fhd(N & F) = err if N > 0 . eq ftl(N & F) = p N & F if N > 0 . end bth 2CHAN-STATE is pr (FAIR-STREAM || FAIR-STREAM) * (sort Tuple to 2ChState). ops (data-ok_) (ack-ok_) : 2ChState -> Bool . ops (fhd1_) (fhd2_) : 2ChState -> Mark . op ftl_ : 2ChState -> 2ChState . vars F F' : FairStream . var Cs : 2ChState . eq fhd1 <F, F'> = fhd F . eq fhd2 <F, F'> = fhd F' . eq ftl <F, F'> = <ftl F, ftl F'> . eq data-ok Cs = eq(fhd1 Cs, ok) . eq ack-ok Cs = eq(fhd2 Cs, ok) . ops (data-ok-after_) (ack-ok-after_) : 2ChState -> 2ChState . eq data-ok-after Cs = data-ok-after ftl Cs if not data-ok Cs . eq data-ok-after Cs = Cs if data-ok Cs . eq ack-ok-after Cs = ack-ok-after ftl Cs if not ack-ok Cs . eq ack-ok-after Cs = Cs if ack-ok Cs . end bth ABP is dsort 2PrState . pr 2CHAN-STATE + STREAM . op <_,_|_,_> : Bool Nat Bool Nat -> 2PrState . op [_,_,_] : 2PrState DataStream 2ChState -> DataStream . vars B B1 B2 : Bool . vars M N : Nat . var Is : DataStream . var Cs : 2ChState . eq [<B,M | B,N>, Is, Cs] = [<B,M | B,N>, Is, ftl Cs] if not ack-ok Cs . eq [<B1,M | B2,N>, Is, Cs] = [<B1,M | B2,N>, Is, ftl Cs] if B1 =/= B2 and not data-ok Cs . eq [<B,M | B,N>, Is, Cs] = [<not B, hd Is | B,N>, tl Is, ftl Cs] if ack-ok Cs . eq tl [<B1,M | B2,N>, Is, Cs] = [<B1,M | B1,M>, Is, ftl Cs] if B1 =/= B2 and data-ok Cs . eq hd [<B1,M | B2,N>, Is, Cs] = N if B1 =/= B2 and data-ok Cs . end ***> here begins the proof <*** bth SETUP is pr ABP . vars-of ABP . op c : -> 2ChState . ops b1 b2 : -> Bool . end ***> proof of Lemma A open . op f : -> FairStream . op n : -> Nat . var Fs : FairStream . red fhd1 data-ok-after <0 & f, Fs> == ok . *** base case eq fhd1 data-ok-after <n & f, Fs> = ok . *** induction step red fhd1 data-ok-after <s n & f, Fs> == ok . close ***> proof of Lemma B open . *** base case eq fhd2 c = err . eq ack-ok-after ftl c = ftl c . red [<B,M | B,N>, Is, c] == [<B,M | B,N>, Is, ack-ok-after ftl c] . close open . *** induction step eq fhd2 c = err . eq fhd2 ftl c = err . red [<B,M | B,N>, Is, ftl c] . *** LHS eq [<B,M | B,N>, Is, ftl ftl c] = [<B,M | B,N>, Is, ack-ok-after ftl ftl c] . red [<B,M | B,N>, Is, c] == [<B,M | B,N>, Is, ack-ok-after ftl c] . close ***> proof of Lemma C open . *** base case eq fhd1 c = err . eq data-ok-after ftl c = ftl c . red [<b1,M | b2,N>, Is, c] == [<b1,M | b2,N>, Is, data-ok-after ftl c] . close open . *** induction step eq fhd1 c = err . eq fhd1 ftl c = err . red [<B1,M | B2,N>, Is, ftl c] . *** LHS eq [<B1,M | B2,N>, Is, ftl ftl c] = [<B1,M | B2,N>, Is, data-ok-after ftl ftl c] if B1 =/= B2 . red [<B1,M | B2,N>, Is, c] == [<B1,M | B2,N>, Is, data-ok-after ftl c] . close set cobasis of STREAM . set cred trace on . ***> proof of Lemma D cases CASE-D for SETUP is vars B B1 B2 : Bool . vars M N P Q : Nat . vars Is Ds : DataStream . var Cs : 2ChState . context [<B,M | B,N>, Is, Cs] . case eq fhd1 ftl Cs = ok . eq fhd2 Cs = ok . case eq fhd1 ftl Cs = err . eq fhd2 Cs = ok . eq [<B1,P | B2, Q>, Ds, ftl ftl Cs] = [<B1,P | B2, Q>, Ds, data-ok-after ftl ftl Cs] if B1 =/= B2 . *** red [<B1,P | B2, Q>, Ds, ftl Cs] . *** LHS end cred with CASE-D [<B,M | B,N>, Is, Cs] == [<not B, hd Is | B,N>, tl Is, data-ok-after ftl Cs] . ***> proof of Lemma E cases CASE-E for SETUP is vars B B1 B2 : Bool . vars M N P Q : Nat . vars Is Ds : DataStream . var Cs : 2ChState . context [<B1,M | B2,N>, Is, Cs] . case eq fhd2 ftl Cs = ok . eq fhd1 Cs = ok . case eq fhd2 ftl Cs = err . eq fhd1 Cs = ok . eq [<B,P | B,Q>, Ds, ftl ftl Cs] = [<B,P | B,Q>, Ds, ack-ok-after ftl ftl Cs] . *** red [<B,P | B,Q>, Ds, ftl Cs] . *** LHS end cred with CASE-E tl [<B1,M | B2,N>, Is, Cs] == [<B1,M | B1,M>, Is, ack-ok-after ftl Cs] if B1 =/= B2 . ***> correctness proof bth ABP+ is dsort 2PrState . pr 2CHAN-STATE + STREAM . op <_,_|_,_> : Bool Nat Bool Nat -> 2PrState . op [_,_,_] : 2PrState DataStream 2ChState -> DataStream . vars B B1 B2 : Bool . vars M N : Nat . var Is : DataStream . var Cs : 2ChState . eq fhd1 data-ok-after Cs = ok . *** A eq [<B,M | B,N>, Is, Cs] = [<B,M | B,N>, Is, ack-ok-after ftl Cs] if not ack-ok Cs . *** B eq [<B1,M | B2,N>, Is, Cs] = [<B1,M | B2,N>, Is, data-ok-after ftl Cs] if B1 =/= B2 and not data-ok Cs . *** C eq [<B,M | B,N>, Is, Cs] = [<not B, hd Is | B,N>, tl Is, data-ok-after ftl Cs] if ack-ok Cs . *** D eq tl [<B1,M | B2,N>, Is, Cs] = [<B1,M | B1,M>, Is, ack-ok-after ftl Cs] if B1 =/= B2 and data-ok Cs . *** E eq hd [<B1,M | B2,N>, Is, Cs] = N if B1 =/= B2 and data-ok Cs . end cases CASE-OF-CHANNEL for ABP+ is vars B1 B2 : Bool . vars N1 N2 : Nat . var Is : DataStream . var Cs : 2ChState . context [<B1,N1 | B2,N2>, Is, Cs] . case eq fhd2 Cs = ok . case eq fhd2 Cs = err . eq fhd2 ack-ok-after ftl Cs = ok . end open . vars B1 B2 : Bool . vars N M : Nat . var Is : DataStream . var Cs : 2ChState . cred with CASE-OF-CHANNEL [<B1,N | B2,M>, Is, Cs] == M & Is if B1 == B2 . close

2. BOBJ Output

awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.204 built: Wed Nov 13 12:40:20 PST 2002 University of California, San Diego Wed Nov 13 18:50:02 PST 2002 BOBJ> in abp ========================================== bth STREAM ========================================== bth FAIR-STREAM ========================================== bth 2CHAN-STATE ========================================== bth ABP ========================================== ***> here begins the proof <*** ========================================== bth SETUP ========================================== ***> proof of Lemma A ========================================== open ========================================== op f : -> FairStream ========================================== op n : -> Nat ========================================== var Fs : FairStream ========================================== reduce in SETUP : fhd1 (data-ok-after (< (0 & f) , Fs >)) == ok result Bool: true rewrite time: 159ms parse time: 21ms ========================================== eq fhd1 (data-ok-after (< (n & f) , Fs >)) = ok ========================================== reduce in SETUP : fhd1 (data-ok-after (< ((s n) & f) , Fs >)) == ok result Bool: true rewrite time: 80ms parse time: 31ms ========================================== close ========================================== ***> proof of Lemma B ========================================== open ========================================== eq fhd2 c = err ========================================== eq ack-ok-after (ftl c) = ftl c ========================================== reduce in SETUP : [(< B , M | B , N >) , Is , c] == [(< B , M | B , N >) , Is , (ack-ok-after (ftl c))] result Bool: true rewrite time: 92ms parse time: 37ms ========================================== close ========================================== open ========================================== eq fhd2 c = err ========================================== eq fhd2 (ftl c) = err ========================================== reduce in SETUP : [(< B , M | B , N >) , Is , (ftl c)] result DataStream: [(< B , M | B , N >) , Is , (ftl (ftl c))] rewrite time: 56ms parse time: 15ms ========================================== eq [(< B , M | B , N >) , Is , (ftl (ftl c))] = [(< B , M | B , N >) , Is , (ack-ok-after (ftl (ftl c)))] ========================================== reduce in SETUP : [(< B , M | B , N >) , Is , c] == [(< B , M | B , N >) , Is , (ack-ok-after (ftl c))] result Bool: true rewrite time: 323ms parse time: 37ms ========================================== close ========================================== ***> proof of Lemma C ========================================== open ========================================== eq fhd1 c = err ========================================== eq data-ok-after (ftl c) = ftl c ========================================== reduce in SETUP : [(< b1 , M | b2 , N >) , Is , c] == [(< b1 , M | b2 , N >) , Is , (data-ok-after (ftl c))] result Bool: true rewrite time: 69ms parse time: 38ms ========================================== close ========================================== open ========================================== eq fhd1 c = err ========================================== eq fhd1 (ftl c) = err ========================================== reduce in SETUP : [(< B1 , M | B2 , N >) , Is , (ftl c)] result DataStream: [(< B1 , M | B2 , N >) , Is , (ftl (ftl c))] rewrite time: 30ms parse time: 15ms ========================================== cq [(< B1 , M | B2 , N >) , Is , (ftl (ftl c))] = [(< B1 , M | B2 , N >) , Is , (data-ok-after (ftl (ftl c)))] if B1 =/= B2 ========================================== reduce in SETUP : [(< B1 , M | B2 , N >) , Is , c] == [(< B1 , M | B2 , N >) , Is , (data-ok-after (ftl c))] result Bool: true rewrite time: 242ms parse time: 38ms ========================================== close ========================================== set cobasis of STREAM ========================================== ***> proof of Lemma D ========================================== cases CASE-D ========================================== c-reduce in SETUP : [(< B , M | B , N >) , Is , Cs] == [(< (not B) , (hd Is) | B , N >) , (tl Is) , (data-ok-after (ftl Cs))] use: CASE-D using cobasis of STREAM: op hd _ : DataStream -> Nat [prec 15] op tl _ : DataStream -> DataStream [prec 15] --------------------------------------- reduced to: [(< B , M | B , N >) , Is , Cs] == [(< (not B) , (hd Is) | B , N >) , (tl Is) , (data-ok-after (ftl Cs))] ----------------------------------------- add rule (C1) : [(< B , M | B , N >) , Is , Cs] = [(< (not B) , (hd Is) | B , N >) , (tl Is) , (data-ok-after (ftl Cs))] ----------------------------------------- target is: [(< B , M | B , N >) , Is , Cs] == [(< (not B) , (hd Is) | B , N >) , (tl Is) , (data-ok-after (ftl Cs))] expand by: op hd _ : DataStream -> Nat [prec 15] reduced to: hd ([(< B , M | B , N >) , Is , Cs]) == hd ([(< (not B) , (hd Is) | B , N >) , (tl Is) , (data-ok-after (ftl Cs))]) ------------------------------------------- case analysis by CASE-D ------------------------------------------- introduce constant(s): b for the variable B n1 for the variable N n for the variable M d for the variable Is %2 for the variable Cs ------------------------------- case 1 : assume: fhd1 (ftl %2) = ok fhd2 %2 = ok reduce: hd ([(< b , n | b , n1 >) , d , %2]) == hd ([(< (not b) , (hd d) | b , n1 >) , (tl d) , (data-ok-after (ftl %2))]) nf: true ------------------------------- case 2 : assume: fhd1 (ftl %2) = err fhd2 %2 = ok [(< B1 , P | B2 , Q >) , Ds , (ftl (ftl %2))] = [(< B1 , P | B2 , Q >) , Ds , (data-ok-after (ftl (ftl %2)))] reduce: hd ([(< b , n | b , n1 >) , d , %2]) == hd ([(< (not b) , (hd d) | b , n1 >) , (tl d) , (data-ok-after (ftl %2))]) nf: true ----------------------------------------- analyzed 2 cases, all cases succeeded ----------------------------------------- target is: [(< B , M | B , N >) , Is , Cs] == [(< (not B) , (hd Is) | B , N >) , (tl Is) , (data-ok-after (ftl Cs))] expand by: op tl _ : DataStream -> DataStream [prec 15] reduced to: tl ([(< B , M | B , N >) , Is , Cs]) == tl ([(< (not B) , (hd Is) | B , N >) , (tl Is) , (data-ok-after (ftl Cs))]) ------------------------------------------- case analysis by CASE-D ------------------------------------------- introduce constant(s): b for the variable B n1 for the variable N n for the variable M d for the variable Is %2 for the variable Cs ------------------------------- case 1 : assume: fhd1 (ftl %2) = ok fhd2 %2 = ok reduce: tl ([(< b , n | b , n1 >) , d , %2]) == tl ([(< (not b) , (hd d) | b , n1 >) , (tl d) , (data-ok-after (ftl %2))]) nf: true ------------------------------- case 2 : assume: fhd1 (ftl %2) = err fhd2 %2 = ok [(< B1 , P | B2 , Q >) , Ds , (ftl (ftl %2))] = [(< B1 , P | B2 , Q >) , Ds , (data-ok-after (ftl (ftl %2)))] reduce: tl ([(< b , n | b , n1 >) , d , %2]) == tl ([(< (not b) , (hd d) | b , n1 >) , (tl d) , (data-ok-after (ftl %2))]) nf: true ----------------------------------------- analyzed 2 cases, all cases succeeded ----------------------------------------- result: true c-rewrite time: 1696ms parse time: 50ms ========================================== ***> proof of Lemma E ========================================== cases CASE-E ========================================== c-reduce in SETUP : tl ([(< B1 , M | B2 , N >) , Is , Cs]) == [(< B1 , M | B1 , M >) , Is , (ack-ok-after (ftl Cs))] if B1 =/= B2 use: CASE-E using cobasis of STREAM: op hd _ : DataStream -> Nat [prec 15] op tl _ : DataStream -> DataStream [prec 15] --------------------------------------- reduced to: tl ([(< B1 , M | B2 , N >) , Is , Cs]) == [(< B1 , M | B1 , M >) , Is , (ack-ok-after (ftl Cs))] if B1 =/= B2 ----------------------------------------- add rule (C1) : tl ([(< B1 , M | B2 , N >) , Is , Cs]) = [(< B1 , M | B1 , M >) , Is , (ack-ok-after (ftl Cs))] if B1 =/= B2 ----------------------------------------- target is: tl ([(< B1 , M | B2 , N >) , Is , Cs]) == [(< B1 , M | B1 , M >) , Is , (ack-ok-after (ftl Cs))] if B1 =/= B2 expand by: op hd _ : DataStream -> Nat [prec 15] reduced to: hd (tl ([(< b1 , M | b2 , N >) , Is , Cs])) == hd ([(< b1 , M | b1 , M >) , Is , (ack-ok-after (ftl Cs))]) ------------------------------------------- case analysis by CASE-E ------------------------------------------- introduce constant(s): n1 for the variable N n for the variable M d for the variable Is %2 for the variable Cs ------------------------------- case 1 : assume: fhd2 (ftl %2) = ok fhd1 %2 = ok reduce: hd (tl ([(< b1 , n | b2 , n1 >) , d , %2])) == hd ([(< b1 , n | b1 , n >) , d , (ack-ok-after (ftl %2))]) nf: true ------------------------------- case 2 : assume: fhd2 (ftl %2) = err fhd1 %2 = ok [(< B , P | B , Q >) , Ds , (ftl (ftl %2))] = [(< B , P | B , Q >) , Ds , (ack-ok-after (ftl (ftl %2)))] reduce: hd (tl ([(< b1 , n | b2 , n1 >) , d , %2])) == hd ([(< b1 , n | b1 , n >) , d , (ack-ok-after (ftl %2))]) nf: true ----------------------------------------- analyzed 2 cases, all cases succeeded condition failed in 0 cases ----------------------------------------- target is: tl ([(< B1 , M | B2 , N >) , Is , Cs]) == [(< B1 , M | B1 , M >) , Is , (ack-ok-after (ftl Cs))] if B1 =/= B2 expand by: op tl _ : DataStream -> DataStream [prec 15] reduced to: tl (tl ([(< b1 , M | b2 , N >) , Is , Cs])) == tl ([(< b1 , M | b1 , M >) , Is , (ack-ok-after (ftl Cs))]) ------------------------------------------- case analysis by CASE-E ------------------------------------------- introduce constant(s): n1 for the variable N n for the variable M d for the variable Is %2 for the variable Cs ------------------------------- case 1 : assume: fhd2 (ftl %2) = ok fhd1 %2 = ok reduce: tl (tl ([(< b1 , n | b2 , n1 >) , d , %2])) == tl ([(< b1 , n | b1 , n >) , d , (ack-ok-after (ftl %2))]) nf: true ------------------------------- case 2 : assume: fhd2 (ftl %2) = err fhd1 %2 = ok [(< B , P | B , Q >) , Ds , (ftl (ftl %2))] = [(< B , P | B , Q >) , Ds , (ack-ok-after (ftl (ftl %2)))] reduce: tl (tl ([(< b1 , n | b2 , n1 >) , d , %2])) == tl ([(< b1 , n | b1 , n >) , d , (ack-ok-after (ftl %2))]) nf: true ----------------------------------------- analyzed 2 cases, all cases succeeded condition failed in 0 cases ----------------------------------------- result: true c-rewrite time: 1686ms parse time: 50ms ========================================== ***> correctness proof ========================================== bth ABP+ ========================================== cases CASE-OF-CHANNEL ========================================== open ========================================== vars B1 B2 : Bool ========================================== vars N M : Nat ========================================== var Is : DataStream ========================================== var Cs : 2ChState ========================================== c-reduce in ABP+ : [(< B1 , N | B2 , M >) , Is , Cs] == M & Is if B1 == B2 use: CASE-OF-CHANNEL using cobasis of STREAM: op hd _ : DataStream -> Nat [prec 15] op tl _ : DataStream -> DataStream [prec 15] --------------------------------------- reduced to: [(< B1 , N | B2 , M >) , Is , Cs] == M & Is if B1 == B2 ----------------------------------------- add rule (C1) : [(< B1 , N | B2 , M >) , Is , Cs] = M & Is if B1 == B2 ----------------------------------------- target is: [(< B1 , N | B2 , M >) , Is , Cs] == M & Is if B1 == B2 expand by: op hd _ : DataStream -> Nat [prec 15] reduced to: hd ([(< b2 , N | b2 , M >) , Is , Cs]) == M ------------------------------------------- case analysis by CASE-OF-CHANNEL ------------------------------------------- introduce constant(s): %2 for the variable Cs d for the variable Is n1 for the variable M n for the variable N ------------------------------- case 1 : assume: fhd2 %2 = ok true = true reduce: hd ([(< b2 , n | b2 , n1 >) , d , %2]) == n1 nf: true ------------------------------- case 2 : assume: fhd2 %2 = err fhd2 (ack-ok-after (ftl %2)) = ok true = true reduce: hd ([(< b2 , n | b2 , n1 >) , d , %2]) == n1 nf: true ----------------------------------------- analyzed 2 cases, all cases succeeded condition failed in 0 cases ----------------------------------------- target is: [(< B1 , N | B2 , M >) , Is , Cs] == M & Is if B1 == B2 expand by: op tl _ : DataStream -> DataStream [prec 15] reduced to: tl ([(< b2 , N | b2 , M >) , Is , Cs]) == Is ------------------------------------------- case analysis by CASE-OF-CHANNEL ------------------------------------------- introduce constant(s): %2 for the variable Cs d for the variable Is n1 for the variable M n for the variable N ------------------------------- case 1 : assume: fhd2 %2 = ok true = true reduce: tl ([(< b2 , n | b2 , n1 >) , d , %2]) == d nf: [(< (not b2) , (hd d) | (not b2) , (hd d) >) , (tl d) , (ack-ok-after (ftl (data-ok-after (ftl %2))))] == d ------------------------------- deduce to : (hd d) & (tl d) == d reduce: tl ([(< b2 , n | b2 , n1 >) , d , %2]) == d nf: true ------------------------------- case 2 : assume: fhd2 %2 = err fhd2 (ack-ok-after (ftl %2)) = ok true = true reduce: tl ([(< b2 , n | b2 , n1 >) , d , %2]) == d nf: [(< (not b2) , (hd d) | (not b2) , (hd d) >) , (tl d) , (ack-ok-after (ftl (data-ok-after (ftl (ack-ok-after (ftl %2))))))] == d ------------------------------- deduce to : (hd d) & (tl d) == d reduce: tl ([(< b2 , n | b2 , n1 >) , d , %2]) == d nf: true ----------------------------------------- analyzed 2 cases, all cases succeeded condition failed in 0 cases ----------------------------------------- result: true c-rewrite time: 2003ms parse time: 32ms ========================================== close BOBJ> q Bye. awk%
To the BOBJ Examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Wed Feb 23 12:33:30 PST 2005