Title :
Modeling and verification of TCP congestion control based on colored Petri nets
Author :
Bao, Ganfeng ; Liu, Fang ; Hong, Li
Author_Institution :
Bell Labs Res., Lucent Technol., Beijing, China
Abstract :
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.
Keywords :
Petri nets; formal verification; graph colouring; operating systems (computers); randomised algorithms; telecommunication congestion control; transport protocols; TCP congestion control; Transport Control Protocol; colored Petri nets; formal model; implementation errors; modeling; occurrence graph; operating systems; randomized algorithm; Additives; Communication system control; Control systems; Error correction; Internet; Operating systems; Petri nets; Resource management; Testing; Transport protocols;
Conference_Titel :
Systems, Man and Cybernetics, 2003. IEEE International Conference on
Print_ISBN :
0-7803-7952-7
DOI :
10.1109/ICSMC.2003.1244550