Formalising TCP's Data Transfer Service Language: A Symbolic Automaton and its Properties

• Autorzy: Billington J. , Han B.
• Języki publikacji: EN

Abstrakty

EN

The TCP/IP protocol suite defines the procedures governing the movement of data within the Internet. A major component of the suite is the Transmission Control Protocol (TCP), which ensures data flows reliably between Internet applications. We use Coloured Petri Nets (CPNs) to model the application's view of the service provided by TCP for the transfer of data. This service depends on the storage capacity available in the Internet. We firstly establish exact expressions for the size of the CPN model's reachability graph (or state space) in terms of the storage capacity. They indicate that both the nodes and arcs of the state space grow exponentially in the storage capacity. Secondly, we derive a symbolic state space which represents an infinite family of state spaces, one for each value of the capacity. We prove that each member of this family is a strongly connected graph and that its associated finite state automaton is deterministic and minimum. Finally, we formulate the TCP data transfer service language for arbitrary capacity, from the symbolic representation of the family of automata. This service language is the yardstick against which the TCP data transfer protocol can be verified with respect to user observable sequences of events.

Słowa kluczowe

EN

TCP; Data Transfer Service; service language; parametric systems; symbolic automata; coloured Petri nets

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 80, nr 1-3
• Strony: 49--74
• Opis fizyczny: bibliogr. 44 poz., wykr.

Twórcy

autor

Billington J.

autor

Han B.

• Computer Systems Engineering Centre School of Electrical and Information Engineering, University of South Australia Mawson Lakes, SA 5095, Australia,

Bibliografia

• [1] W.A. Barrett, R.M. Bates, D.A. Gustafson, and J.D. Couch. Compiler Construction: Theory and Practice. Science Research Associates, 2nd edition, 1986.
• [2] J. Billington. Abstract Specification of the ISO Transport Service Definition using Labelled Numerical Petri Nets. In Protocol Specification, Testing, and Verification, III, pages 173-185. Elsevier Science Publishers, 1983.
• [3] J. Billington. Discrete Event Systems Theory and its Application to Command and Control. CSEC Report 14, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Australia, December 2002.
• [4] J. Billington, M. Diaz, and G. Rozenberg, editors. Application of Petri nets to Communication Networks: Advances in Petri nets, volume 1605 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1999.
• [5] J. Billington, G.E. Gallasch, and B. Han. A Coloured Petri Net Approach to Protocol Verification. In Lecture Notes in Computer Science: Lectures on Concurrency and Petri Nets, volume 3098, pages 210-290. Springer, Berlin, June 2004.
• [6] J. Billington and B. Han. Formalising the TCP Symmetrical Connection Management Service. In Proc. Design, Analysis and Simulation of Distributed Systems Conference, Orlando, Florida, USA, pages 178-184, March 2003.
• [7] J. Billington and B. Han. On Defining the Service Provided by TCP. In Proc. 26th Australasian Computer Science Conference, Adelaide, Australia, volume 16 of Conferences in Research and Practice in Information Technology, pages 129-138, February 2003.
• [8] J. Billington and B. Han. Closed Form Expressions for the State Space of TCP's Data Transfer Service Operating over Unbounded Channels. In Proc. 27th Australasian Computer Science Conference, Dunedin, New Zealand, volume 26 of Conferences in Research and Practice in Information Technology, pages 31-39, January 2004.
• [9] J. Billington and B. Han. Modelling and Analysing the Functional Behaviour of TCP's Connection Management Procedures. International Journal on Software Tools for Technology Transfer, May 2007. in press, available at http://dx.doi.org/10.1007/s10009-007-0034-1.
• [10] J. Billington, M. C. Wilbur-Ham, and M. Y. Bearman. Automated Protocol Verification. In Protocol Specification, Testing, and Verification, V, pages 59-70. Elsevier Science Publishers, 1986.
• [11] D. E. Cass and M. T. Rose. ISO Transport Services on Top of the TCP. RFC 983, IETF, April 1986.
• [12] Computer Systems Engineering Centre. Web site: http://www.unisa.edu.au/csec.
• [13] R. Fielding, J. Gettys, J. Mogul, H. Frystyk, L. Masinter, P. Leach, and T. Berners-Lee. Hypertext Transfer Protocol - HTTP/1.1. RFC 2616, IETF, June 1999.
• [14] G. E. Gallasch and J. Billington. Using Parametric Automata for the Verification of the Stop and Wait Class of Protocols. In Proc. 3rd Int. Symposium on Automated Technology for Verification and Analysis, volume 3707 of Lecture Notes in Computer Science, pages 457-473, Taipei, Taiwan, October 2005. Springer.
• [15] G. E. Gallasch and J. Billington. A Parametric State Space for the Analysis of the Infinite Class of Stop-and- Wait Protocols. In Proc. 13th International SPIN Workshop on Model Checking Software, volume 3925 of Lecture Notes in Computer Science, pages 201-218, Vienna, Austria, March 2006. Springer.
• [16] B. Han. Formal Specification of the TCP Service and Verification of TCP Connection Management. PhD Thesis, University of South Australia, Australia, December 2004.
• [17] B. Han and J. Billington. An Analysis of TCP Connection Management Using Coloured Petri Nets. In Proc. 5th World Multi-Conference on Systemics, Cybernetics and Informatics (SCI'2001), pages 590-595, Orlando, Florida, July 2001.
• [18] B. Han and J. Billington. Validating TCP Connection Management. In Proc. Workshop on Software Engineering and Formal Methods, Adelaide, Australia, volume 12 of Conferences in Research and Practice in Information Technology, pages 47-55, June 2002.
• [19] B. Han and J. Billington. Termination Properties of TCP's Connection Management Procedures. In Proc. 26th Int. Conf. Application and Theory of Petri Nets and Other Models of Concurrency, volume 3536 of Lecture Notes in Computer Science, pages 228-249,Miami, Florida, USA, June 2005. Springer.
• [20] F. Harary. Graph Theory. Addison-Wesley, 1969.
• [21] J. E. Hopcroft, R. Motwani, and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, U.S.A, 2nd edition, 2001.
• [22] Internet Engineering Task Force. Web site: http://www.ietf.org.
• [23] ISO/IEC, Software and System Engineering - High-level Petri Nets-Part 1: Concepts, Definitions and Graphical Notation. International Standard ISO/IEC 15909-1, December 2004.
• [24] ITU-T. Information Technology - Open Systems Interconnection - Basic Reference Model: Conventions for the Definition of OSI Services, November 1993. ITU-T Recommendation X.210.
• [25] ITU-T. Information Technology - Open Systems Interconnection - Transport Service Definition, November 1995. ITU-T Recommendation X.214.
• [26] K. Jensen. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 1, Basic Concepts. Springer-Verlag, Berlin, 1997.
• [27] K. Jensen. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 2, Analysis Methods. Springer-Verlag, Berlin, 1997.
• [28] K. Jensen. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 3, Practical Use. Springer-Verlag, Berlin, 1997.
• [29] L. Liu and J. Billington. Tackling the Infinite State Space of a Multimedia Control Protocol Service Specification. In Proc. 23rd International Conference on Application and Theory of Petri Nets, volume 2360 of Lecture Notes in Computer Science, pages 273-293, Adelaide, Australia, 2002. Springer.
• [30] L. Liu and J. Billington. Obtaining the Service Language for H.245's Multimedia Capability Exchange Signalling Protocol: the Final Step. In Proc. 10th International Multimedia Modelling Conference, pages 323-328, Brisbane, Australia, January 2004. IEEE Computer Society.
• [31] L. Liu and J. Billington. Reducing Parametric Automata: A Multimedia Protocol Service Case Study. In Proc. 2nd Int. Symposium on Automated Technology for Verification and Analysis, volume 3299 of Lecture Notes in Computer Science, pages 483-486, Taipei, Taiwan, 2004. Springer.
• [32] S. L. Murphy. Service Specification and Protocol Construction for a Layered Architecture. PhD Thesis, University of Maryland, USA, May 1990.
• [33] S. L. Murphy and A. U. Shankar. Connection Management for the Transport Layer: Service Specification and Protocol Verification. IEEE Transactions on Communications, 39(12):1762-1775, December 1991.
• [34] V. Paxson. Known TCP Implementation Problems. RFC 2525, IETF, March 1999.
• [35] J. L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice-Hall, Englewood Cliffs, NJ, 1981.
• [36] J. Postel. Transmission Control Protocol. RFC 793, IETF, September 1981.
• [37] Y. Pouffary and A. Young. ISO Transport Service on top of TCP (ITOT). RFC 2126, IETF, March 1997.
• [38] M. T. Rose and D. E. Cass. ISO Transport Service on Top of the TCP Version: 3. RFC 1006, IETF, May 1987.
• [39] M. A. Smith. Formal Verification of Communication Protocols. In Formal Description Techniques IX: Theory, Applications and Tools, pages 129-144. Chapman & Hall, London, UK, October 1996.
• [40] M. A. Smith. Formal Verification of TCP and T/TCP. PhD Thesis, M.I.T., USA, September 1997.
• [41] A. S. Tanenbaum. Computer Networks. Prentice Hall, 4th edition, 2003.
• [42] J. D. Ullman. Elements of ML Programming. Prentice Hall, Englewood Cliffs, NJ, 2nd edition, 1998.
• [43] University of Aarhus. Design/CPN Online. Web site: http://www.daimi.au.dk/designCPN, 2003.
• [44] C. A. Vissers and L. Logrippo. The Importance of the Service Concept in the Design of Data Communications Protocols. In Protocol Specification, Testing, and Verification, V, pages 3-17. Elsevier Science Publishers, 1986.