Abstract
The well-known Sliding Window protocol caters for the reliable and efficient transmission of data over unreliable channels that can lose, reorder and duplicate messages. Despite the practical importance of the protocol and its high potential for errors, it has never been formally verified for the general setting. We try to fill this gap by giving a fully formal specification and verification of an improved version of the protocol. The protocol is specified by a timed state machine in the language of the verification system PVS. This allows a mechanical check of the proof by the interactive proof checker of PVS. Our modelling is very general and includes such important features of the protocol as sending and receiving windows of arbitrary size, bounded sequence numbers and channels that may lose, reorder and duplicate messages.
This research is supported by the Dutch PROGRESS project EES5202, “Modelling and performance analysis of telecommunication systems”.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Y. Afek, H. Attiya, A. Fekete, M. Fischer, N. Lynch, Y. Mansour, D. Wang, and L. Zuck. Reliable communication over unreliable channels. Journal of the ACM, 41:1267–1297, 1994.
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
M.A. Bezem and J.F. Groote. A correctness proof of a one-bit sliding window protocol in μCRL. The Computer Journal, 37:1–19, 1994.
K.A. Barlett, R.A. Scantlebury, and P.C. Wilkinson. A note on reliable transmission over half duplex links. Communications of the ACM, 12:260–261, 1969.
D. Chkliaev. Mechanical Verification of Concurrency Control and Recovery Protocols. PhD thesis, Technische Universiteit Eindhoven, 2001.
P.R. D’Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In TACAS’97, pages 416–431. LNCS 1217, 1997.
W. Fokkink, J.F. Groote, and J. Pang. Verification of a sliding window protocol in μCRL. Unfinished article, 2003.
J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. A case study in computer-checked verification. In AMAST’96, pages 536–550. LNCS 1101, 1996.
T. Hune, J.M.T. Romijn, M.I.A. Stoelinga, and F.W. Vaandrager. Linear parametric model checking of timed automata. In TACAS’01, pages 189–203. LNCS 2031, 2001.
K. Havelund and N. Shankar. Experiments in Theorem Proving and Model Checking for Protocol Verification. In FME’96: Industrial Benefit and Advances in Formal Methods, pages 662–681. LNCS 1051, 1996.
L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In International Workshop TYPES’93, pages 127–165. LNCS 806, 1994.
R. Kaivola. Using compositional preorders in the verification of sliding window protocol. In Computer Aided Verification, pages 48–59. LNCS 1254, 1997.
D.E. Knuth. Verification of link-level protocols. BIT, 21:31–36, 1981.
N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.
PVS Specification and Verification System, http://pvs.csl.sri.com/ .
J.L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Verification in Xesar of the sliding window protocol. In Protocol specification, testing and verification 7, pages 235–248, 1987.
K. Stahl, K. Baukus, Y. Lakhnech, and M. Steffen. Divide, abstract, and model-check. In The 5th International SPIN Workshop on Theoretical Aspects of Model Checking, pages 57–76. LNCS 1680, 1999.
C. Sunshine and Y. Dalal. Connection management in transport protocols. Computer Networks, 2:454–473, 1978.
A. Udaya Shankar. Verified data transfer protocols with variable flow control. ACM Transactions on Computer Systems, 7:281–316, 1989.
M. Smith and N. Klarlund. Verification of a sliding window protocol using IOA and MONA. In Formal methods for distributed system development, pages 19–34. Kluwer Academic Publishers, 2000.
N.V. Stenning. A data transfer protocol. Computer Networks, 1:99–110, 1976.
A.S. Tanenbaum. Computer Networks. Third Edition, Prentice-Hall International, 1996.
PVS specifications and proofs, http://www.cs.kun.nl/~hooman/SWP.html .
D. Wang and L. Zuck. Tight bounds for the sequence transmission problem. In The 8th ACM Symposium on Principles of Distributed Computing, pages 73–83. ACM, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chkliaev, D., Hooman, J., de Vink, E. (2003). Verification and Improvement of the Sliding Window Protocol. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_9
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive