Modeling and verification of TCP congestion control based on colored Petri nets

There are different TCP congestion control implementations running on different operating systems. The implementation errors are easily introduced and have been reported by a RFC. It is a challenging task to ensure that TCP protocol is correctly and completely implemented according to the specification. This paper focuses on TCP congestion control modeling and verification. A verification environment is presented and a formal model of the TCP congestion control is established using colored Petri nets. The controllable and observable events in the verification environment are encoded in the model. The verification is performed by searching the occurrence graph of the model. A randomized algorithm is adopted to verify the TCP congestion control implementations.