In: Conferences in Research and Practice in Information Technology, Vol.12, Workshop on Software Engineering and Formal Methods, pages 47-55. 24-25 June 2002. Australian Computer Society Inc., Adelaide.
Abstract: The Internet's Transmission Control Protocol (TCP) is specified informally in Request For Comments (RFC) 793 but still lacks a formal specification. 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.
Keywords: TCP Connection Management; Coloured Petri Nets; Design/CPN; Finite State Machine; Reachability Analysis.
Back to the Petri Nets Bibliography