DocumentCode :
398006
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
Volume :
2
fYear :
2003
fDate :
5-8 Oct. 2003
Firstpage :
1045
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Systems, Man and Cybernetics, 2003. IEEE International Conference on
ISSN :
1062-922X
Print_ISBN :
0-7803-7952-7
Type :
conf
DOI :
10.1109/ICSMC.2003.1244550
Filename :
1244550
Link To Document :
بازگشت