| The Transmission Control Protocol (TCP) was designed to provide a reliable end-to-end connection between two hosts. Over time, it has become the de facto transport layer protocol in the Internet. It is important to thoroughly understand the resilience behavior of TCP in the case of network congestion and failure and improve the resilience performance of TCP if possible.; We studied the detailed resilience behavior of SACK, NewReno, and Reno TCP, and recommended the proper resilience objectives for TCP transport in the Internet. Specifically, with SACK TCP, we found two restoration objectives, tau 1,S and tau2,S. With NewReno TCP, we also found two restoration objectives, tau1,NR and tau2,NR. tau1,NR is approximately twice as large as tau1,S when rwnd is large. tau2,NR is essentially the same as tau 2,S. With Reno TCP, we found a recovery objective of 200ms for the DS0 access; for DS1 and OC-3c access, there seem to be no critical points from 15ms to 1s.; After understanding the detailed behavior of SACK TCP, we proposed two types of mechanisms, Probing and Pacing, to improve the resilience of SACK TCP. SACK TCP with Probing and Pacing were modeled with Petri nets. The Petri net models were formally analyzed to increase our confidence about the correctness of the proposed changes. Our experimental results demonstrate that SACK TCP with Probing and Pacing is much more resilient than standard SACK TCP.; To test the effectiveness of the proposed protocols, we proposed a hybrid protocol development methodology, embedding formal models into simulation, that combines the use of formal methods and simulation to obtain the advantages of deep formal verification with the broad spectrum testing of simulation. With the assistance of this hybrid methodology, we tested alpha-min Paced SACK TCP in a NSF-like network. The results show that alpha-min Paced SACK TCP performs better than SACK TCP in terms of resilience, not only in single session scenarios, but also in multiple session cases, even if these TCP sessions have varied RTTs. |
