Coloured Petri Net Modelling of an Evolving Internet Standard: the Datagram Congestion Control Protocol

• Autorzy: Billington J. , Vanit-Anunchai S.
• Języki publikacji: EN

Abstrakty

EN

The DatagramCongestion Control Protocol (DCCP) is a new transport protocol standardized by the Internet Engineering Task Force (IETF) in March 2006. This paper discusses the specification of the connectionmanagement and synchronization procedures of DCCP using Coloured Petri Nets (CPNs). After introducing the protocol, we describe how the CPN model evolved as DCCP was being developed. We focus on our experience of incremental enhancement in the hope that this will provide guidance to those attempting to build complex protocol models. In particular, we discuss how the architecture, data structures and specification style of the model evolved as DCCP was developed. We finally recommend a procedure-based style once the standard is stable. The impact of this work on the DCCP standard and our interaction with IETF is also briefly discussed.

Słowa kluczowe

EN

Internet Protocols; Datagram Congestion Control Protocol (DCCP); coloured Petri nets; formal specifications; Evolutionary Modelling

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 88, nr 3
• Strony: 357--385
• Opis fizyczny: bibliogr. 29 poz., tab., wykr.

Twórcy

autor

Billington J.

autor

Vanit-Anunchai S.

• Computer Systems Engineering Centre, University of South Australia, Mawson Lakes, SA, 5095, Australia,

Bibliografia

• [1] J. Billington, M. Diaz, and G. Rozenberg (Eds.). Application of Petri Nets to Communication Networks, volume 1605 of Lecture Notes in Computer Science. Springer, Heidelberg, 1999.
• [2] J. Billington, G. E. Gallasch, and B. Han. A Coloured Petri Net Approach to Protocol Verification. In J. Desel, W. Reisig, and G. Rozenberg, editors, Lectures on Concurrency and Petri Nets, Advances in Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 210-290. Springer, Heidelberg, 2004.
• [3] J. Billington and B. Han. Modelling and Analysing the Functional Behaviour of TCP's ConnectionManagement Procedures. International Journal on Software Tools for Technology Transfer, 9(3-4):269-304, June 2007. Available via http://dx.doi.org/10.1007/s10009-007-0034-1.
• [4] DCCP home page. http://www.read.cs.ucla.edu/dccp/.
• [5] S. Floyd, M. Handley, and E. Kohler. Problem Statement for the Datagram Congestion Control Protocol (DCCP), RFC 4336. Available via http://www.rfc-editor.org/rfc/rfc4336.txt,March 2006.
• [6] S. Floyd and E. Kohler. Profile for Datagram Congestion Control Protocol (DCCP) Congestion Control ID 2: TCP-like Congestion Control, RFC 4341. Available via http://www.rfc-editor.org/rfc/rfc4341.txt,March 2006.
• [7] S. Floyd, E. Kohler, and J. Padhye. Profile for Datagram Congestion Control Protocol (DCCP) Congestion Control ID 3: TCP-Friendly Rate Control (TFRC), RFC 4342. Available via http://www.rfceditor. org/rfc/rfc4342.txt,March 2006.
• [8] G.E. Gallasch, J. Billington, S. Vanit-Anunchai, and L.M. Kristensen. Checking Safety Properties On-The-Fly with the Sweep-line Method. International Journal on Software Tools for Technology Transfer, 9(3-4):374-391, June 2007. Available via http://dx.doi.org/10.1007/s10009-007-0031-4.
• [9] ITU. Specification and Description Language (SDL), ITU-T Recommendation Z.100 (08/2002). International Telecommunication Union, 2003.
• [10] K. Jensen. Coloured Petri Nets: Basic Concepts, AnalysisMethods and PracticalUse. Vol. 1, Basic Concepts. Monographs in Theoretical Computer Science. Springer, Heidelberg, 2nd edition, 1997.
• [11] K. Jensen, L.M. Kristensen, and L. Wells. Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. International Journal on Software Tools for Technology Transfer, 9(3-4):213-254, June 2007.
• [12] E. Kohler,M. Handley, and S. Floyd. Designing DCCP: Congestion ControlWithout Reliability. In Proceedings of the 2006 ACM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (SIGCOMM'06), pages 27-38, Pisa, Italy, 11-15 September 2006.
• [13] E. Kohler, M. Handley, and S. Floyd. Datagram Congestion Control Protocol, draft-ietf-dccp-spec-6. Available via http://www.read.cs.ucla.edu/dccp/draft-ietf-dccp-spec-06.txt, February 2004.
• [14] E. Kohler, M. Handley, and S. Floyd. Datagram Congestion Control Protocol, draft-ietf-dccp-spec-7. Available via http://www.read.cs.ucla.edu/dccp/draft-ietf-dccp-spec-07.txt, July 2004.
• [15] E. Kohler,M. Handley, and S. Floyd. Datagram Congestion Control Protocol, draft-ietf-dccp-spec-11. Available via http://www.read.cs.ucla.edu/dccp/draft-ietf-dccp-spec-11.txt,March 2005.
• [16] E. Kohler, M. Handley, and S. Floyd. SUBSTANTIVE DIFFERENCES BETWEEN draft-ietf-dccp-spec-11 AND draft-ietf-dccp-spec-12. Available via http://www.read.cs.ucla.edu/dccp/diff-spec-11-12-explain.txt, December 2005.
• [17] E. Kohler, M. Handley, and S. Floyd. Datagram Congestion Control Protocol, RFC 4340. Available via http://www.rfc-editor.org/rfc/rfc4340.txt,March 2006.
• [18] E. Kohler, M. Handley, and S. Floyd. SUBSTANTIVE DIFFERENCES BETWEEN draft-ietf-dccp-spec-13 AND RFC 4340. Available via http://www.read.cs.ucla.edu/dccp/diff-spec-13-rfc-explain.txt,March 2006.
• [19] E. Kohler, M. Handley, S. Floyd, and J. Padhye. Datagram Congestion Control Protocol, draft-ietf-dccpspec- 5. Available via http://www.read.cs.ucla.edu/dccp/draft-ietf-dccp-spec-05.txt, October 2003.
• [20] T. Kongprakaiwoot. Verification of the Datagram Congestion Control Protocol using Coloured Petri Nets. Master's thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia, November 2004.
• [21] J. Postel. Transmission Control Protocol (TCP), RFC793. Available via http://www.rfceditor. org/rfc/rfc793.txt, September 1981.
• [22] University of Aarhus. Design/CPN Online, 2004. Available via http://www.daimi.au.dk/designCPN/.
• [23] S. Vanit-Anunchai and J. Billington. Effect of Sequence Number Wrap on DCCP Connection Establishment. In Proceedings of the 14th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS), pages 345-354,Monterey, California, USA, 11-13 September 2006. IEEE Computer Society Press.
• [24] S. Vanit-Anunchai and J. Billington. Initial Result of a Formal Analysis of DCCP Connection Management. In Proceedings of the Fourth International Network Conference (INC 2004), pages 63-70, Plymouth, UK, 6-9 July 2004. University of Plymouth.
• [25] S. Vanit-Anunchai and J. Billington. Chattering Behaviour in the Datagram Congestion Control Protocol. IEE Electronics Letters, 41(21):1198-1199,October 2005.
• [26] S. Vanit-Anunchai and J. Billington. Modelling the Datagram Congestion Control Protocol's Connection Management and Synchronisation Procedures. In J. Kleijn and A. Yakovlev, editors, Proceedings of the 28th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN'07), volume 4546 of Lecture Notes in Computer Science, pages 423-444, Siedlce, Poland, 25-29 June 2007. Springer, Heidelberg.
• [27] S. Vanit-Anunchai, J. Billington, and G.E. Gallasch. Analysis of the Datagram Congestion Control Protocol's Connection Management Procedures using the Sweep-lineMethod. International Journal on Software Tools for Technology Transfer, 10(1):29-56, 2008. Available via http://dx.doi.org/10.1007/s10009-007-0050-1.
• [28] S. Vanit-Anunchai, J. Billington, and G.E. Gallasch. Sweep-lineAnalysis of DCCP ConnectionManagement. In Seventh Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB-579, pages 157-175.Department of Computer Science, University of Aarhus, 24-26 October 2006. Available via http://www.daimi.au.dk/CPnets/workshop06/cpn/papers/.
• [29] S. Vanit-Anunchai, J. Billington, and T. Kongprakaiwoot. Discovering Chatter and Incompleteness in the Datagram Congestion Control Protocol. In F. Wang, editor, Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2005), volume 3731 of Lecture Notes in Computer Science, pages 143-158, Taipei, Taiwan, 2-5 October 2005. Springer, Heidelberg.