A Correctness Proof of a One-bit Sliding Window Protocol in CRL
Open Access
- 1 January 1994
- journal article
- Published by Oxford University Press (OUP) in The Computer Journal
- Vol. 37 (4) , 289-307
- https://doi.org/10.1093/comjnl/37.4.289
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.Keywords
This publication has 0 references indexed in Scilit: