Verification of a sliding window protocol in μ CRL and PVS
Bahareh Badban, Wan J. Fokkink, Jan Friso Groote, Jun Pang, Jaco van de Pol · Formal Aspects of Computing · 2005
Abstract We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2 n . The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2 n . The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS.