university website

W.J. Fokkink (Wan), J.F. Groote (Jan Friso), J. Pang, B. Badban (Bahareh) and J.C. van de Pol (Jaco)

2003

Verifying a sliding window protocol in mCRL

Publication

Publication

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.

Additional Metadata
ACM Requirements/Specifications (acm D.2.1), Network Protocols (acm C.2.2), Specifying and Verifying and Reasoning about Programs (acm F.3.1)
MSC Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (msc 68N30), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)
THEME Software (theme 1)
Publisher CWI
Series Software Engineering [SEN]
Organisation Software Analysis and Transformation
Citation
Fokkink, W., Groote, J. F., Pang, J., Badban, B., & van de Pol, J. (2003). Verifying a sliding window protocol in mCRL. Software Engineering [SEN]. CWI.
Free Full Text ( Final Version , 846kb ) cover


User Publication Person Organisation Collection
Close