%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
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.
Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org