Mechanical verification of a two-way sliding window protocol

Badban, Bahareh and Fokkink, Wan and Pol van de, Jaco (2008) Mechanical verification of a two-way sliding window protocol. In: Communicating Process Architectures 2008, 7-10 September 2008, York, UK.

PDF
Restricted to UT campus only: Request a copy
286Kb

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 muCRL. 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).
Item Type:	Conference or Workshop Item
Copyright:	© 2008 IOS Press
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/62463
Official URL:	http://dx.doi.org/10.3233/978-1-58603-907-3-179
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 251185