An elementary derivation of the alternating bit protocol

W.H.J. Feijen, A.J.M. Gasteren, van, B. Schieder

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)
1 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationMathematics of Program Construction (Proceedings 4th International Conference, MPC'98, Marstrand, Sweden, July 15-17, 1998)
EditorsJ. Jeuring
Place of PublicationBerlin
PublisherSpringer
Pages175-187
ISBN (Print)3-540-64591-8
DOIs
Publication statusPublished - 1998

Publication series

NameLecture Notes in Computer Science
Volume1422
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'An elementary derivation of the alternating bit protocol'. Together they form a unique fingerprint.

Cite this