For the most recent entries see the Petri Nets Newsletter.

Formalising the TCP Symmetrical Connection Management Service.

Billington, J.; Han, B.

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography