Validating TCP connection management
Bing Han, Jonathan Billington · 2002
The Internet's Transmission Control Protocol (TCP) is speci- ed informally in Request For Comments (RFC) 793 but still lacks a formal speci cation. This paper presents a formal model of TCP connection management using coloured Petri nets (CPNs). The model is used to examine certain properties (e.g., the absence of deadlocks and correct message sequences) of TCP and to check the internal consistency of RFC 793. In this paper, problems with some informal descriptions in RFC 793 concerning simultaneous open have been discovered through automated reachability analysis. Corrections to the problems have been proposed and tested.