Mechanical verification of a two-way sliding window protocol

Bahareh Badban, Wan Fokkink, Jan Cornelis van de Pol

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

    3 Citations (Scopus)


    We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgments of the latest received data are attached to the next data transmitted back into the channel. The window size of both parties are considered to be finite, though they can be of different sizes. We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of muCRL. We use the theorem prover PVS to formalize and to mechanically prove the correctness. This implies both safety and liveness (under the assumption of fairness).
    Original languageUndefined
    Title of host publicationCommunicating Process Architectures 2008
    EditorsP.H. Welch, F.A.C. Polack, F.R.M. Barnes, A.A. McEwan, G.S. Stiles, Johannes F. Broenink, A.T. Sampson
    Place of PublicationAmsterdam
    PublisherIOS Press
    Number of pages24
    ISBN (Print)978-1-58603-907-3
    Publication statusPublished - Sep 2008
    EventCommunicating Process Architectures, CPA 2008: 31st WoTUG Conference on Concurrent and Parallel Programming - York, United Kingdom
    Duration: 7 Sep 200810 Sep 2008
    Conference number: 31

    Publication series

    NameConcurrent Systems Engineering Series
    PublisherIOS Press


    ConferenceCommunicating Process Architectures, CPA 2008
    Country/TerritoryUnited Kingdom


    • CR-D.2.4
    • METIS-251185
    • EWI-13441
    • IR-62463

    Cite this