Verification of a sliding window protocol in mCRL and PVS

B. Badban; W.J. Fokkink; J.F. Groote; J. Pang; J.C. van de Pol

doi:10.1007/s00165-005-0070-0

Verification of a sliding window protocol in mCRL and PVS

B. Badban
, W.J. Fokkink
, J.F. Groote
, J. Pang
, J.C. van de Pol

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS. © BCS 2005.

Original language	English
Pages (from-to)	342-388
Journal	Formal Aspects of Computing
Volume	17
Issue number	3
DOIs	https://doi.org/10.1007/s00165-005-0070-0
Publication status	Published - 2005

Bibliographical note

DBLP:journals/fac/BadbanFGPP05

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Access to Document

10.1007/s00165-005-0070-0

Persistent URL (handle)

Persistent link

Cite this

@article{0d5c9b35b77e4ac397cbb1d27feaac79,

title = "Verification of a sliding window protocol in mCRL and PVS",

abstract = "We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS. {\textcopyright} BCS 2005.",

author = "B. Badban and W.J. Fokkink and J.F. Groote and J. Pang and \{van de Pol\}, J.C.",

note = "DBLP:journals/fac/BadbanFGPP05 ",

year = "2005",

doi = "10.1007/s00165-005-0070-0",

language = "English",

volume = "17",

pages = "342--388",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery (ACM)",

number = "3",

}

TY - JOUR

T1 - Verification of a sliding window protocol in mCRL and PVS

AU - Badban, B.

AU - Fokkink, W.J.

AU - Groote, J.F.

AU - Pang, J.

AU - van de Pol, J.C.

N1 - DBLP:journals/fac/BadbanFGPP05

PY - 2005

Y1 - 2005

N2 - We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS. © BCS 2005.

AB - We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS. © BCS 2005.

U2 - 10.1007/s00165-005-0070-0

DO - 10.1007/s00165-005-0070-0

M3 - Article

SN - 0934-5043

VL - 17

SP - 342

EP - 388

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 3

ER -

Verification of a sliding window protocol in mCRL and PVS

Abstract

Bibliographical note

UN SDGs

Access to Document

Persistent URL (handle)

Fingerprint

Cite this