Verification and improvement of the sliding window protocol

D. Chkliaev, J.J.M. Hooman, E.P. Vink, de

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

30 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems (Proceedings TACAS 2003, Warsaw, Poland, April 7-11, 2003)
EditorsH. Garavel, J. Hatcliff
Place of PublicationBerlin
PublisherSpringer
Pages113-127
ISBN (Print)3-540-00898-5
DOIs
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science
Volume2619
ISSN (Print)0302-9743

    Fingerprint

Cite this

Chkliaev, D., Hooman, J. J. M., & Vink, de, E. P. (2003). Verification and improvement of the sliding window protocol. In H. Garavel, & J. Hatcliff (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (Proceedings TACAS 2003, Warsaw, Poland, April 7-11, 2003) (pp. 113-127). (Lecture Notes in Computer Science; Vol. 2619). Berlin: Springer. https://doi.org/10.1007/3-540-36577-X_9