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

15 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
PublisherFormal Methods and Tools (FMT)
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

Badban, B., Fokkink, W., & van de Pol, J. C. (2008). Mechanical Verification of a Two-Way Sliding Window Protocol (Full version including proofs). (CTIT Technical Report Series; No. 302/TR-CTIT-08-45). Enschede: Formal Methods and Tools (FMT).
Badban, Bahareh ; Fokkink, Wan ; van de Pol, Jan Cornelis. / Mechanical Verification of a Two-Way Sliding Window Protocol (Full version including proofs). Enschede : Formal Methods and Tools (FMT), 2008. 55 p. (CTIT Technical Report Series; 302/TR-CTIT-08-45).
@book{e5140b6f2f5745dfa09bcce5529858bc,
title = "Mechanical Verification of a Two-Way Sliding Window Protocol (Full version including proofs)",
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 = "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",
author = "Bahareh Badban and Wan Fokkink and {van de Pol}, {Jan Cornelis}",
year = "2008",
month = "6",
day = "30",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Formal Methods and Tools (FMT)",
number = "302/TR-CTIT-08-45",

}

Badban, B, Fokkink, W & van de Pol, JC 2008, Mechanical Verification of a Two-Way Sliding Window Protocol (Full version including proofs). CTIT Technical Report Series, no. 302/TR-CTIT-08-45, Formal Methods and Tools (FMT), Enschede.

Mechanical Verification of a Two-Way Sliding Window Protocol (Full version including proofs). / Badban, Bahareh; Fokkink, Wan; van de Pol, Jan Cornelis.

Enschede : Formal Methods and Tools (FMT), 2008. 55 p. (CTIT Technical Report Series; No. 302/TR-CTIT-08-45).

Research output: Book/ReportReportProfessional

TY - BOOK

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

AU - Badban, Bahareh

AU - Fokkink, Wan

AU - van de Pol, Jan Cornelis

PY - 2008/6/30

Y1 - 2008/6/30

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 - a pair of FIFO queues

KW - CR-F.3.1

KW - specification in μCRL

KW - IR-64845

KW - METIS-251045

KW - verificationwith PVS

KW - EWI-12976

KW - Two-way sliding window protocol

M3 - Report

T3 - CTIT Technical Report Series

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

PB - Formal Methods and Tools (FMT)

CY - Enschede

ER -

Badban B, Fokkink W, van de Pol JC. Mechanical Verification of a Two-Way Sliding Window Protocol (Full version including proofs). Enschede: Formal Methods and Tools (FMT), 2008. 55 p. (CTIT Technical Report Series; 302/TR-CTIT-08-45).