Skip to main content
SpringerLink
Log in

Validating DCCP Simultaneous Feature Negotiation Procedure

  • Chapter
  • First Online:
Transactions on Petri Nets and Other Models of Concurrency XI

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 9930))

Abstract

This paper investigates the feature negotiation procedure of the Datagram Congestion Control Protocol (DCCP) in RFC 4340 using Coloured Petri Nets (CPNs). After obtaining a formal executable CPN model of DCCP feature negotiation, we analyse it using state spaces. The experimental result reveals that simultaneous negotiation may be incorrect and broken on even a lossless FIFO channel. In the undesired terminal states, the confirmed feature values of the client and the server do not match. To fix this problem we suggest two solutions. Firstly, sending a Change option when an endpoint changes its preference. Secondly, an endpoint in STABLE does not discard non-reordered Confirm options. We have applied our suggested changes to the constructed CPN models. The formal verification of the revised models shows that the undesired terminal states have been eliminated.

This work is supported by Research Grant no. TRG5380023 from the Thai Network Information Center Foundation and the Thailand Research Fund.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    It is difficult to justify the consequence when the CCIDs of both side do not match because it depends on the applications. However, we envisage that the receiver could submit garbage to the application while no one realizes the problem.

  2. 2.

    The solution that fixes errors in an environment may cause other errors in a different environment.

References

  1. Babich, F., Deotto, L.: Formal methods for the specification, analysis of communication protocols. IEEE Commun. Surv. 4(1), 2–20 (2002). Third Quarter

    Article  Google Scholar 

  2. Billington, J., Diaz, M., Rozenberg, G. (eds.): Application of Petri Nets to Communication Networks. LNCS, vol. 1605. Springer, Heidelberg (1999)

    Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Billington, J., Vanit-Anunchai, S., Gallasch, G.E.: Parameterised Coloured Petri Net channel models. Trans. Petri Nets Other Models Concurrency 3, 71–97 (2009)

    Article  Google Scholar 

  5. CPN Tools home page. http://cpntools.org

  6. Figueiredo, J.C.A., Kristensen, L.M.: Using Coloured Petri Nets to investigate behavioural and performance issues of TCP protocols. In: Second Workshop and Tutorial on Practical Use of Coloured Petri Nets and Design/CPN, DAIMI PB-541, pp. 21–40. Department of Computer Science, University of Aarhus, 11–15 October 1999

    Google Scholar 

  7. Floyd, S., Handley, M., Kohler, E.: Problem statement for the Datagram Congestion Control Protocol (DCCP), RFC 4336, March 2006. http://www.rfc-editor.org/rfc/rfc4336.txt

  8. Floyd, S., Kohler, E., Profile for Datagram Congestion Control Protocol (DCCP) congestion control ID 2: TCP-like congestion control, RFC 4341, March 2006. http://www.rfc-editor.org/rfc/rfc4341.txt

  9. Floyd, S., Kohler, E.: Profile for Datagram Congestion Control Protocol (DCCP) congestion control ID 4: TCP-Friendly Rate Control for Small Packets (TFRC-SP), RFC 5622, August 2009. http://www.rfc-editor.org/rfc/rfc5622.txt

  10. Floyd, S., Kohler, E., Padhye, J., Profile for Datagram Congestion Control Protocol (DCCP) congestion control ID 3: TCP-Friendly Rate Control (TFRC), RFC 4342, March 2006. http://www.rfc-editor.org/rfc/rfc4342.txt

  11. Gordon, S.: Verification of the WAP transaction layer using Coloured Petri Nets. Ph.D. thesis, Institute for Telecommunications Research and Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia, November 2001

    Google Scholar 

  12. Han, B.: Formal specification of the TCP service and verification of TCP connection management. Ph.D. thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia, December 2004

    Google Scholar 

  13. Jensen, K., Kristensen, L.M.: Colored Petri Nets: a graphical language for formal modeling and validation of concurrent systems. Commun. ACM 58(6), 61–70 (2015)

    Article  Google Scholar 

  14. Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009)

    Book  MATH  Google Scholar 

  15. Kohler, E., Handley, M., Floyd, S.: Designing DCCP: congestion control without reliability. In: Proceedings of the 2006 ACM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (SIGCOMM 2006), pp. 27–38, Pisa, Italy, 11–15 September 2006

    Google Scholar 

  16. Kohler, E., Handley, M., Floyd, S.: Datagram Congestion Control Protocol, RFC 4340, March 2006. http://www.rfc-editor.org/rfc/rfc4340.txt

  17. Kristensen, L.M., Inge, K., Simonsen, F.: Applications of Coloured Petri Nets for functional validation of protocol designs. Trans. Petri Nets Other Models Concurrency 7, 56–115 (2013)

    MATH  Google Scholar 

  18. Kristensen, L.M., Jørgensen, J.B., Jensen, K.: Application of Coloured Petri Nets in system development. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 626–685. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. University of Aberdeen, Electronics Research Group, School of Engineering: Background on Feature Negotiation. http://www.erg.abdn.ac.uk/users/gerrit/dccp/notes/feature_negotiation/background.html

  21. University of Aberdeen, Electronics Research Group, School of Engineering: Why feature negotiation and protocol state machine are not independent. http://www.erg.abdn.ac.uk/users/gerrit/dccp/notes/feature_negotiation/dependencies.html

  22. Vanit-Anunchai, S.: An investigation of the datagram congestion control protocol’s connection management and synchronisation procedures. Ph.D. thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia, November 2007

    Google Scholar 

  23. Vanit-Anunchai, S.: Analysis of two-layer protocols: DCCP simultaneous-open and hole punching procedures. In: Choppy, C., Sun, J. (eds.) 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). OpenAccess Series in Informatics (OASIcs), vol. 31, pp. 3–17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2013)

    Google Scholar 

  24. Vanit-Anunchai, S.: Validating SCTP simultaneous open procedure. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 233–249. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  25. Vanit-Anunchai, S., Billington, J., Gallasch, G.E.: Analysis of the datagram congestion control protocol’s connection management procedures using the sweep-line method. Int. J. Softw. Tools Technol. Transfer 10(1), 29–56 (2008). http://dx.doi.org/10.1007/s10009-007-0050-1

    Article  Google Scholar 

  26. Vanit-Anunchai, S., Billington, J., Kongprakaiwoot, T.: Discovering chatter and incompleteness in the datagram congestion control protocol. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 143–158. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Acknowledgements

This work is supported by Research Grant no. TRG5380023 from the Thai Network Information Center Foundation and the Thailand Research Fund. The author is thankful to anonymous reviewers. Their constructive feedback has helped the author improve the quality of this paper.

Author information

Authors and Affiliations

  1. School of Telecommunication Engineering, Institute of Engineering, Suranaree University of Technology, Nakhon Ratchasima, 30000, Thailand

    Somsak Vanit-Anunchai

Authors
  1. Somsak Vanit-Anunchai
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Somsak Vanit-Anunchai .

Editor information

Editors and Affiliations

  1. Newcastle University , Newcastle upon Tyne, United Kingdom

    Maciej Koutny

  2. FernUniversität in Hagen , Hagen, Germany

    Jörg Desel

  3. Leiden University , Leiden, The Netherlands

    Jetty Kleijn

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Vanit-Anunchai, S. (2016). Validating DCCP Simultaneous Feature Negotiation Procedure. In: Koutny, M., Desel, J., Kleijn, J. (eds) Transactions on Petri Nets and Other Models of Concurrency XI. Lecture Notes in Computer Science(), vol 9930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53401-4_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-53401-4_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-53400-7

  • Online ISBN: 978-3-662-53401-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation