Mechanical verification of a two-way sliding window protocol

Bahareh Badban; Wan Fokkink; Jan Cornelis van de Pol

doi:10.3233/978-1-58603-907-3-179

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 proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

1 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 language	Undefined
Title of host publication	Communicating Process Architectures 2008
Editors	P.H. Welch, F.A.C. Polack, F.R.M. Barnes, A.A. McEwan, G.S. Stiles, Johannes F. Broenink, A.T. Sampson
Place of Publication	Amsterdam
Publisher	IOS
Pages	179-202
Number of pages	24
ISBN (Print)	978-1-58603-907-3
DOIs	https://doi.org/10.3233/978-1-58603-907-3-179
Publication status	Published - Sept 2008
Event	Communicating Process Architectures, CPA 2008: 31st WoTUG Conference on Concurrent and Parallel Programming - York, United Kingdom Duration: 7 Sept 2008 → 10 Sept 2008 Conference number: 31

Publication series

Name	Concurrent Systems Engineering Series
Publisher	IOS Press
Number	Supplement
Volume	66

Conference

Conference	Communicating Process Architectures, CPA 2008
Country/Territory	United Kingdom
City	York
Period	7/09/08 → 10/09/08

Keywords

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

Access to Document

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

http://eprints.eemcs.utwente.nl/secure2/13441/01/piggybacking.pdf

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). Article 10.3233/978-1-58603-907-3-179 (Concurrent Systems Engineering Series; Vol. 66, No. Supplement). IOS. 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, 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 ; Communicating Process Architectures, CPA 2008 ; Conference date: 07-09-2008 Through 10-09-2008",

year = "2008",

month = sep,

doi = "10.3233/978-1-58603-907-3-179",

language = "Undefined",

isbn = "978-1-58603-907-3",

series = "Concurrent Systems Engineering Series",

publisher = "IOS",

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, 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, 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 proceeding › Conference contribution › Academic › peer-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 - Conference code: 31

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

CY - Amsterdam

T2 - Communicating Process Architectures, CPA 2008

Y2 - 7 September 2008 through 10 September 2008

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. 2008. p. 179-202. 10.3233/978-1-58603-907-3-179. (Concurrent Systems Engineering Series; Supplement). doi: 10.3233/978-1-58603-907-3-179