Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published January 1, 1991 | Accepted Version
Report Open

The Sliding Window Protocol Revisited

Abstract

We 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.

Attached Files

Accepted Version - 91-06.pdf

Accepted Version - postscript.ps

Files

91-06.pdf
Files (506.4 kB)
Name Size Download all
md5:29e2c52638d0c856d0031b878bb0c32f
379.9 kB Preview Download
md5:1fe492c392688932bd5d203742a411c5
126.5 kB Download

Additional details

Created:
August 22, 2023
Modified:
December 22, 2023