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.