In: Proc. 2003 Design, Analysis, and Simulation of Distributed Systems, pages 178-184. 2003. 30 March - 3 April 2003, Orlando, USA.
Abstract: The Transmission Control Protocol (TCP) is an important building block of the Internet protocol suite (TCP/IP). It is therefore of interest to know what service it provides to its users. This paper extends previous work on defining the TCP service by including the simultaneous opening of connections and formalises the service using coloured Petri nets. The global sequences of the service primitives are generated using reachability analysis and automata reduction techniques. The impact of the simultaneous open and aborting connections on the number of global sequences is investigated. The service formalised in this paper is an essential step in verifying TCP.
Keywords: TCP connection management; service definition; finite state automata; coloured Petri nets; reachability analysis.