Published on Sep 03, 2023
The Sliding Window (SW) protocol has been widely used in many popular communication protocols. The protocol can ensure a correct data transfer over very poor quality communication channels where the packets may be duplicated, lost, or re-ordered .A number of parameters affects the performance characteristics of the SW protocol. Usually, these performance characteristics cannot be determined analytically.
However, we need to study these key performance characteristics and to identify optimal parameter settings in the early design phases when parameter settings in the early design phases when designing an adaptive algorithm or novel protocols for specific computing environments. Such information is helpful for the designer to work out a product.
In this paper we introduce the sliding window protocol generally, describe the communication procedure of the protocol, and conclude some related parameters affecting the overall performance of the system. In order to estimate the performance of the SW protocol systematically, as an exercise, an abstract executable performance model of the protocol using go back n is created in POOSL.
The model allows us to present and analyze some performance characteristics. These performance characteristics include the throughput (the bandwidth utilization) of the protocol and the delay of the acknowledgement. Some key-parameters such as the window size, the timeout period, the round trip time, the packet size, and the probability of packets loss are investigated in several network environments and different parameter settings as well.
Reliable transmission of data over unreliable channels is an old and well-studied problem in computer science. Without a satisfactory solution, computer networks would be useless, because they transmit data over channels that often lose, duplicate, or reorder messages. One of the most efficient protocols for reliable transmission is the Sliding Window (SW) protocol. Many popular communication protocols such as TCP and HDLC are based on the SW protocol.
Communication protocols usually involve a subtle interaction of a number of distributed components and have a high degree of parallelism. This is why their correctness is difficult to ensure, and many protocols turned out to be erroneous. One of the most promising solutions to this problem is the use of formal verification, which requires the precise specification of the protocol in some specification language and a formal proof of its correctness by mathematical techniques.
Despite the practical significance of the Sliding Window protocol, the work on its formal verification had only a limited success so far. Stunning only gave an informal manual proof for his protocol. A semi-formal manual proof is also presented in.
A more formal, but not fully automated proof for the window size of one is given in, and for the arbitrary window size in. Some versions of the protocol have been model-checked for small parameter values.
The combination of abstraction techniques and model-checking in allowed verifying the SW protocol for a relatively large window size of 16 (which is still a few orders less than a possible window size in TCP). Almost all of these verifications assume data link channels , which can only lose messages.
The protocols for such channels, called data link protocols , are important (they include, e.g., HDLC, SLIP and PPP protocols), but they are only used for transmission of data over relatively short distances. The verification of sliding window protocols for more general transport channels , which can also reorder and duplicate messages. Such channels are already considered in the original paper on the SW protocol by Stenning
