Formal Verification of an Improved Sliding Window Protocol
D. Chkliaev, J. Hoomand and E. de Vink

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 
full 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 number and
channels that may lose, reorder and duplicate messages.