Verification of a Timestamp-Based Sliding-Window Protocol

摘要

The authors present the verification and analysis of a sliding-window protocolwhich uses sequence numbers and timestamps to achieve reliable, flow-controlled data transfer over an unreliable network. The timestamps are used to prevent hazards present in very high-speed networks due to the too fast wrap-around of sequence numbers. The protocol the authors analyze in this paper models the PAWS (protect against wrapped sequence numbers) mechanism, a proposed extension of the Transmission Control Protocol (TCP) of the Internet protocol suite. Some modifications are made on the original proposal to eliminate a possible hazard which was revealed during the formal analysis and to extend it with selective acknowledgements. The protocol is specified as an event-driven system using a system model which is capable to express real-time properties, such as packet lifetimes in the network, maximum transmission rate and clock skew. The authors take into account that both sequence numbers and timestamps are represented as finite numbers and give sufficient conditions for the safe reuse of these identifiers. Informal arguments about the sharpness of the sufficient conditions are also presented.