Verifying a Sliding-Window Protocol Using PVS
Vlad Rusu · Kluwer Academic Publishers eBooks · 2006
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. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.