V. Rusu. Verifying a sliding-window protocol using PVS. In Formal Techniques
for Networked and Distributed Systems (FORTE'01) , 2001, pp 251-266, 2001.

Abstract:
We present the deductive verification of safety and liveness properties
of a sliding-window protocol using the PVS theorem prover. The protocol
is modeled in an operational style which is close to an actual  program.
It has parametric window sizes for both sender and receiver, and unbounded
lossy communication channels  carrying unbounded data. The proofs are done
using invariant strengthening techniques encoded as PVS automated strategies
based on heuristics and decision procedures.

PVS files:
To load the files, just copy the file sliding_window.dmp on your machine,
then start PVS 2.3, and type undump-pvs-files. This will create the following
hierarchy of theories: sliding_window_liveness imports sliding_window_safety,
which imports sliding_window, which imports both Action and runs.

You can rerun the proofs in each theory by typing ESC-x prt. If this is done
in the right order, i.e., starting from runs and Action to the higher-level
theories, you will obtain the status that each lemma and theorem is completely
proved. Enjoy!