A correctness proof of a one-bit sliding window protocol in µCRL

M.A. Bezem; J.F. Groote

doi:10.1093/comjnl/37.4.289

A correctness proof of a one-bit sliding window protocol in µCRL

M.A. Bezem
, J.F. Groote

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

20 Citations (Scopus)

4 Downloads (Pure)

Abstract

We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in µCRL, which is a process algebra extended with data. Due to the abundant parallelism in this protocol, the behaviour is quite complicated. The complexity has been mastered by explicitly identifying invariants and foci of cones in the protocol. Both concepts seem promising as tools for the verification of larger and more complex protocols.

Original language	English
Pages (from-to)	289-307
Number of pages	19
Journal	The Computer Journal
Volume	37
Issue number	4
DOIs	https://doi.org/10.1093/comjnl/37.4.289
Publication status	Published - 1994

Access to Document

10.1093/comjnl/37.4.289

Cite this

@article{bb7fa302f6fb459d989097c996ebf039,

title = "A correctness proof of a one-bit sliding window protocol in µCRL",

abstract = "We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in µCRL, which is a process algebra extended with data. Due to the abundant parallelism in this protocol, the behaviour is quite complicated. The complexity has been mastered by explicitly identifying invariants and foci of cones in the protocol. Both concepts seem promising as tools for the verification of larger and more complex protocols.",

author = "M.A. Bezem and J.F. Groote",

year = "1994",

doi = "10.1093/comjnl/37.4.289",

language = "English",

volume = "37",

pages = "289--307",

journal = "The Computer Journal",

issn = "0010-4620",

publisher = "Oxford University Press",

number = "4",

}

TY - JOUR

T1 - A correctness proof of a one-bit sliding window protocol in µCRL

AU - Bezem, M.A.

AU - Groote, J.F.

PY - 1994

Y1 - 1994

N2 - We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in µCRL, which is a process algebra extended with data. Due to the abundant parallelism in this protocol, the behaviour is quite complicated. The complexity has been mastered by explicitly identifying invariants and foci of cones in the protocol. Both concepts seem promising as tools for the verification of larger and more complex protocols.

AB - We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in µCRL, which is a process algebra extended with data. Due to the abundant parallelism in this protocol, the behaviour is quite complicated. The complexity has been mastered by explicitly identifying invariants and foci of cones in the protocol. Both concepts seem promising as tools for the verification of larger and more complex protocols.

U2 - 10.1093/comjnl/37.4.289

DO - 10.1093/comjnl/37.4.289

M3 - Article

SN - 0010-4620

VL - 37

SP - 289

EP - 307

JO - The Computer Journal

JF - The Computer Journal

IS - 4

ER -

A correctness proof of a one-bit sliding window protocol in µCRL

Abstract

Access to Document

Fingerprint

Cite this