Verification and Improvement of the Sliding Window Protocol
Dmitri Chkliaev,
Jozef Hooman
and Erik de Vink
Appeared in:
Proc. 9th Conference on
Tools and Algorithms for the Construction
and Analysis of Systems (TACAS'03) , LNCS 2619,
Springer-Verlag,
pages 113-127, 2003.
ABSTRACT
The well-known Sliding Window protocol
caters for the reliable and efficient transmission of data
over unreliable channels that can lose, reorder and duplicate messages.
Despite the practical importance of the protocol
and its high potential for errors,
it has never been formally verified for the general setting.
We try to fill this gap by giving a fully formal specification and
verification of an improved version of the protocol.
The protocol is specified by a timed state machine in the language of the
verification system
PVS.
This allows a mechanical check of the proof by the
interactive proof checker of PVS.
Our modelling is very general
and includes such important features of the protocol as sending and receiving
windows of arbitrary size, bounded sequence numbers and
channels that may lose, reorder and duplicate messages.
Paper in
pdf
and
postscript © Springer-Verlag
Specification in PVS language
PVS dump file with all proofs
An earlier version appeared in the Proc. of the 3d PROGRESS Workshop on
Embedded Systems, Technology Foundation STW, pages 18-27, 2002.
pdf