In: Kung-Kiu Lau, Richard Banach (Eds.): Lecture Notes in Computer Science, 3785: Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005., pages 156-172. Springer-Verlag, October 2005. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1157628012,.
Abstract: Despite the widespread use of the Transmission Control Protocol (TCP) as the main transport protocol in the Internet, the procedures for connection establishment and release are still not fully understood. This paper extends the analysis of a Coloured Petri net model of TCP's Connection Management procedures by applying the state explosion alleviation technique known as the sweep-line method. The protocol is assumed to be operating over a reordering lossless channel. Termination and absence of deadlock properties are investigated for many scenarios, including client-server and simultaneous connection establishment, orderly release and abortion. The sweep-line method provides a reduction in memory usage of around a factor of 10 and allows investigation of many scenarios that were previously out of the reach of conventional methods.
Keywords: TCP Connection Management, State Space methods, Reachability analysis, Sweep-line analysis, Coloured Petri Nets, Verification..