We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory.

, ,
,
CWI
Software Engineering [SEN]
Software Analysis and Transformation

Fokkink, W.J, Groote, J.F, Pang, J, Badban, B, & van de Pol, J.C. (2003). Verifying a sliding window protocol in mCRL. Software Engineering [SEN]. CWI.