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)

    Abstract

    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
    Pages179-202
    Number of pages24
    ISBN (Print)978-1-58603-907-3
    DOIs
    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
    NumberSupplement
    Volume66

    Conference

    ConferenceCommunicating Process Architectures, CPA 2008
    CountryUnited Kingdom
    CityYork
    Period7/09/0810/09/08

    Keywords

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

    Cite this

    Badban, B., Fokkink, W., & van de Pol, J. C. (2008). Mechanical verification of a two-way sliding window protocol. In P. H. Welch, F. A. C. Polack, F. R. M. Barnes, A. A. McEwan, G. S. Stiles, J. F. Broenink, & A. T. Sampson (Eds.), Communicating Process Architectures 2008 (pp. 179-202). [10.3233/978-1-58603-907-3-179] (Concurrent Systems Engineering Series; Vol. 66, No. Supplement). Amsterdam: IOS Press. https://doi.org/10.3233/978-1-58603-907-3-179
    Badban, Bahareh ; Fokkink, Wan ; van de Pol, Jan Cornelis. / Mechanical verification of a two-way sliding window protocol. Communicating Process Architectures 2008. editor / P.H. Welch ; F.A.C. Polack ; F.R.M. Barnes ; A.A. McEwan ; G.S. Stiles ; Johannes F. Broenink ; A.T. Sampson. Amsterdam : IOS Press, 2008. pp. 179-202 (Concurrent Systems Engineering Series; Supplement).
    @inproceedings{900c41d5e19e47e0aa387ae191f52c61,
    title = "Mechanical verification of a two-way sliding window protocol",
    abstract = "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).",
    keywords = "CR-D.2.4, METIS-251185, EWI-13441, IR-62463",
    author = "Bahareh Badban and Wan Fokkink and {van de Pol}, {Jan Cornelis}",
    note = "10.3233/978-1-58603-907-3-179",
    year = "2008",
    month = "9",
    doi = "10.3233/978-1-58603-907-3-179",
    language = "Undefined",
    isbn = "978-1-58603-907-3",
    series = "Concurrent Systems Engineering Series",
    publisher = "IOS Press",
    number = "Supplement",
    pages = "179--202",
    editor = "P.H. Welch and F.A.C. Polack and F.R.M. Barnes and A.A. McEwan and G.S. Stiles and Broenink, {Johannes F.} and A.T. Sampson",
    booktitle = "Communicating Process Architectures 2008",
    address = "Netherlands",

    }

    Badban, B, Fokkink, W & van de Pol, JC 2008, Mechanical verification of a two-way sliding window protocol. in PH Welch, FAC Polack, FRM Barnes, AA McEwan, GS Stiles, JF Broenink & AT Sampson (eds), Communicating Process Architectures 2008., 10.3233/978-1-58603-907-3-179, Concurrent Systems Engineering Series, no. Supplement, vol. 66, IOS Press, Amsterdam, pp. 179-202, Communicating Process Architectures, CPA 2008, York, United Kingdom, 7/09/08. https://doi.org/10.3233/978-1-58603-907-3-179

    Mechanical verification of a two-way sliding window protocol. / Badban, Bahareh; Fokkink, Wan; van de Pol, Jan Cornelis.

    Communicating Process Architectures 2008. ed. / P.H. Welch; F.A.C. Polack; F.R.M. Barnes; A.A. McEwan; G.S. Stiles; Johannes F. Broenink; A.T. Sampson. Amsterdam : IOS Press, 2008. p. 179-202 10.3233/978-1-58603-907-3-179 (Concurrent Systems Engineering Series; Vol. 66, No. Supplement).

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

    TY - GEN

    T1 - Mechanical verification of a two-way sliding window protocol

    AU - Badban, Bahareh

    AU - Fokkink, Wan

    AU - van de Pol, Jan Cornelis

    N1 - 10.3233/978-1-58603-907-3-179

    PY - 2008/9

    Y1 - 2008/9

    N2 - 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).

    AB - 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).

    KW - CR-D.2.4

    KW - METIS-251185

    KW - EWI-13441

    KW - IR-62463

    U2 - 10.3233/978-1-58603-907-3-179

    DO - 10.3233/978-1-58603-907-3-179

    M3 - Conference contribution

    SN - 978-1-58603-907-3

    T3 - Concurrent Systems Engineering Series

    SP - 179

    EP - 202

    BT - Communicating Process Architectures 2008

    A2 - Welch, P.H.

    A2 - Polack, F.A.C.

    A2 - Barnes, F.R.M.

    A2 - McEwan, A.A.

    A2 - Stiles, G.S.

    A2 - Broenink, Johannes F.

    A2 - Sampson, A.T.

    PB - IOS Press

    CY - Amsterdam

    ER -

    Badban B, Fokkink W, van de Pol JC. Mechanical verification of a two-way sliding window protocol. In Welch PH, Polack FAC, Barnes FRM, McEwan AA, Stiles GS, Broenink JF, Sampson AT, editors, Communicating Process Architectures 2008. Amsterdam: IOS Press. 2008. p. 179-202. 10.3233/978-1-58603-907-3-179. (Concurrent Systems Engineering Series; Supplement). https://doi.org/10.3233/978-1-58603-907-3-179