The famous alternating bit protocol is an algorithm for transmitting a sequence of data through a so-called faulty channel, i.e. a channel that can lose or duplicate injected data. The established literature provides a wealth of treatments and plenty of a-posteriori correctness proofs of the protocol; derivations of the algorithm, however, are very rare. The prime purpose of this note is to provide such a derivation from first principles, using the theory of Owicki and Gries as the only tool for reasoning about parallel programs.
|Title of host publication||Mathematics of Program Construction (Proceedings 4th International Conference, MPC'98, Marstrand, Sweden, July 15-17, 1998)|
|Place of Publication||Berlin|
|Publication status||Published - 1998|
|Name||Lecture Notes in Computer Science|