Verification of a sliding window protocol in μCRL and PVS

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 axiom...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2005-10, Vol.17 (3), p.342-388
Main Authors: BADBAN, Bahareh, FOKKINK, Wan, GROOTE, Jan Friso, JUN PANG, VAN DE POL, Jaco
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-005-0070-0