In: Gianfranco Ciardo, Philippe Darondeau (Eds.): Lecture Notes in Computer Science, Vol. 3536: Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005., pages 228-249. Springer Verlag, June 2005.
Abstract: The Transmission Control Protocol (TCP) is the most widely used transport protocol in the Internet, providing a reliable data transfer service to many applications. This paper analyses TCP's Connection Management procedures for correct termination and absence of deadlocks. The protocol is assumed to be operating over a reordering lossless channel and is modelled using Coloured Petri nets. The following connection management scenarios are examined using state space analysis: client-server and simultaneous opening; orderly release; and abortion. The results demonstrate that TCP terminates correctly for client-server and simultaneous connection establishment, orderly release after the connection is established and aborting of connections. However, we discover a deadlock when connection release is initiated before the connection has been fully established when operating over a reordering lossless channel.