Formalising the TCP Symmetrical Connection Management Service

摘要

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.