Paper Details

@InProceedings{Badban08,
  title = "{M}echanical {V}erification of a {T}wo-{W}ay {S}liding {W}indow {P}rotocol",
  author= "Badban, Bahareh and Fokkink, Wan and Van De Pol, Jaco",
  editor= "Welch, Peter H. and Stepney, S. and Polack, F.A.C and Barnes, Frederick R. M. and McEwan, Alistair A. and Stiles, G. S. and Broenink, Jan F. and Sampson, Adam T.",
  pages = "179--202",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2008",
  isbn= "978-1-58603-907-3",
  year= "2008",
  month= "sep",
  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 \textlessi\textgreaterpair of
     FIFO\textless/i\textgreater 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.