A Correctness Proof of a One-bit Sliding Window Protocol in CRL | Zendy

M. A. Bezem | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Correctness Proof of a One-bit Sliding Window Protocol in CRL

Author(s) -

M. A. Bezem

Publication year - 1994

Publication title -

the computer journal

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.319

H-Index - 64

eISSN - 1460-2067

pISSN - 0010-4620

DOI - 10.1093/comjnl/37.4.289

Subject(s) - correctness , sliding window protocol , protocol (science) , computer science , window (computing) , parallelism (grammar) , bit (key) , theoretical computer science , process (computing) , algorithm , distributed computing , parallel computing , computer network , programming language , operating system , medicine , alternative medicine , pathology

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research