Verifying a Sliding Window Protocol in Emphasis T

Authors: Wan Fokkink Jan Friso Groote Jun Pang Bahareh Badban Jaco van de Pol

Publish Date: 2004/7/12

Volume: , Issue: , Pages: 148-163

PDF Link

Abstract

We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n We show 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 was checked with the help of PVS

Keywords: