Mechanical Verification of a Two-Way Sliding Window Protocol (Full version including proofs)

Bahareh Badban, Wan Fokkink, Jan Cornelis van de Pol

    Research output: Book/ReportReportProfessional

    74 Downloads (Pure)

    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
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages55
    Publication statusPublished - 30 Jun 2008

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.302/TR-CTIT-08-45
    ISSN (Print)1381-3625

    Keywords

    • a pair of FIFO queues
    • CR-F.3.1
    • specification in μCRL
    • IR-64845
    • METIS-251045
    • verificationwith PVS
    • EWI-12976
    • Two-way sliding window protocol

    Cite this