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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Allman, M., Paxson, V., Stevens, W.: TCP Congestion Control. RFC 2581 (April 1999)
Billington, J., Gallasch, G.E., Han, B.: A Coloured Petri Net Approach to Protocol Verification. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 210–290. Springer, Heidelberg (2004)
Braden, R.: Requirements for Internet Host – Communication Layers. RFC 1122 (October 1989)
Burdett, D.: Internet Open Trading Protocol - IOTP Version 1.0. RFC 2801, IETF (April 2000)
Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)
Stewart, R., et al.: Stream Control Transmission Protocol. RFC 2960 (October 2000)
Paxson, V., et al.: Known TCP Implementation Problems. RFC 2525 (March 1999)
Floyd, S.: HighSpeed TCP for Large Congestion Windows. RFC 3649 (December 2003)
Floyd, S., Henderson, T.: The NewReno Modification to TCP’s Fast Recovery Algorithm. RFC 2582 (April 1999)
Gallasch, G.E., Ouyang, C., Billington, J., Kristensen, L.M.: Experimenting with Progress Mappings for the Application of the Sweep-Line Analysis fo the Internet Open Trading Protocol. In: Fifth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, University of Aarhus. Department of Computer Science (2004), Available via http://www.daimi.au.dk/CPnets/workshop04/cpn/papers/
Gordon, S., Kristensen, L.M., Billington, J.: Verification of a Revised WAP Wireless Transaction Protocol. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 182–202. Springer, Heidelberg (2002)
Han, B.: Formal Specification of the TCP Service and Verification of TCP Connection Management. PhD thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia (December 2004)
Han, B., Billington, J.: Termination Properties of TCP’s Connection Management Procedures. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 228–249. Springer, Heidelberg (2005)
Jacobson, V., Braden, R.: TCP Extensions for Long Delay Paths. RFC 1072 (October 1988)
Jacobson, V., Braden, R., Borman, D.: TCP Extensions for High Performance. RFC 1323 (May 1992)
Jacobson, V., Braden, R., Zhang, L.: TCP Extension for High-Speed Paths. RFC 1185 (October 1990)
Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Vol. 1, Basic Concepts, 2nd edn. Springer, Heidelberg (1997)
Kohler, E., Handley, M., Floyd, S.: Datagram Congestion Control Protocol. draft-ietf-dccp-spec-11 (March 2005)
Kristensen, L.M., Christensen, S., Jensen, K.: The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer 2(2), 98–132 (1998)
Kristensen, L.M., Mailund, T.: A Generalised Sweep-Line Method for Safety Properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549–567. Springer, Heidelberg (2002)
Postel, J.: Transmission Control Protocol. RFC 793 (September 1981)
Sunshine, C.A., Dalal, Y.K.: Connection Management in Transport Protocols. Computer Networks 2(6), 346–350 (1978)
Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Wright, G.R., Stevens, W.R.: TCP/IP Illustrated, Vol. 2: The Implementation. Addison-Wesley, Reading (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gallasch, G.E., Han, B., Billington, J. (2005). Sweep-Line Analysis of TCP Connection Management. In: Lau, KK., Banach, R. (eds) Formal Methods and Software Engineering. ICFEM 2005. Lecture Notes in Computer Science, vol 3785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11576280_12
Download citation
DOI: https://doi.org/10.1007/11576280_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29797-0
Online ISBN: 978-3-540-32250-4
eBook Packages: Computer ScienceComputer Science (R0)