Paper Details

%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 μ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).

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.