The Sliding Window Protocol RevisitedVan de Snepscheut, Jan L. A. (1991) The Sliding Window Protocol Revisited. Technical Report. California Institute of Technology. [CaltechCSTR:1991.cs-tr-91-06] Full text available as:
AbstractWe give a correctness proof of the sliding window protocol. Both safety and liveness properties are addressed. We show how faulty channels can be represented as nondeterministic programs. The correctness proof is given as a sequence of correctness-preserving transformations of a sequential program that satisfies the original specification, with the exception that it does not have any faulty channels. We work as long as possible with a sequential program, although the transformation steps are guided by the aim of going to a distributed program. The final transformation steps consist in distributing the actions of the sequential program over a number of processes.
Archive Staff Only: edit this record |