%T Mechanical Verification of a Two\-Way Sliding Window Protocol
%A  Bahareh Badban,  Wan Fokkink,  Jaco Van De Pol
%E Peter H. Welch,  S. Stepney,  F.A.C Polack,  Frederick R. M. Barnes,  Alistair A. McEwan,  G. S. Stiles,  Jan F. Broenink,  Adam T. Sampson
%B Communicating Process Architectures 2008
%X 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 <i>pair of FIFO</i> 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).