Verification of a sliding window protocol in mCRL and PVS

B. Badban, W.J. Fokkink, J.F. Groote, J. Pang, J.C. van de Pol

Research output: Contribution to JournalArticleAcademicpeer-review


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, and has been checked in the theorem prover PVS. © BCS 2005.
Original languageEnglish
Pages (from-to)342-388
JournalFormal Aspects of Computing
Issue number3
Publication statusPublished - 2005

Bibliographical note



Dive into the research topics of 'Verification of a sliding window protocol in mCRL and PVS'. Together they form a unique fingerprint.

Cite this