Paper Details

Communicating Process Architectures (CPA)
 Title: Mechanical Verification of a Two-Way Sliding Window Protocol
 Conference: Communicating Process Architectures 2008
 Authors: Bahareh Badbana, Wan Fokkinkb, Jaco van de Polc
(a) Department of Computer and Information Science, University of Konstanz
(b) Department of Computer Science, Vrije Universiteit Amsterdam
(c) Department of EEMCS, University of Twente
 Abstract: We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgments of the latest received data are attached to the next data transmitted back into the channel. The window size of both parties are considered to be finite, though they can be of different sizes. We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of mu-CRL. We use the theorem prover PVS to formalize and to mechanically prove the correctness. This implies both safety and liveness (under the assumption of fairness). 

BibTeX Entry

Full paper