Specification and verification of the classical sliding window protocol

We consider the well-known Sliding Window Protocol (SWP) which provides reliable and efficient transmission of data over unreliable channels. It seems quite important to give a formal proof of correctness for the SWP, especially because the high degree of parallelism in this protocol creates a significant potential for errors. However, the efforts to provide a deductive verification for the SWP had only a limited success so far. To fill this gap, we offer a new approach, in which the protocol is specified by a state machine in the language of the verification system PVS. We also formalize its safety property and prove it using the interactive proof checker of PVS.