Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Validating DCCP Simultaneous Feature Negotiation Procedure

Author : Somsak Vanit-Anunchai

Published in: Transactions on Petri Nets and Other Models of Concurrency XI

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Non-interference Notions Based on Reveals and Excludes Relations for Petri Nets
next chapter Integrating Petri Net Semantics in a Model-Driven Approach: The Renew Meta-Modeling and Transformation Framework
Footnotes
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
The solution that fixes errors in an environment may cause other errors in a different environment.
 
Literature
1.
Babich, F., Deotto, L.: Formal methods for the specification, analysis of communication protocols. IEEE Commun. Surv. 4(1), 2–20 (2002). Third QuarterCrossRef
2.
Billington, J., Diaz, M., Rozenberg, G. (eds.): Application of Petri Nets to Communication Networks. LNCS, vol. 1605. Springer, Heidelberg (1999)
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)CrossRef
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)CrossRef
5.
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
7.
8.
9.
10.
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
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
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)CrossRef
14.
Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009)CrossRefMATH
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
16.
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
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)CrossRef
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)CrossRef
20.
21.
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
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)
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)CrossRef
25.
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)CrossRef
Metadata
Title
Validating DCCP Simultaneous Feature Negotiation Procedure
Author
Somsak Vanit-Anunchai
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Transactions on Petri Nets and Other Models of Concurrency XI

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

Electronic ISBN: 978-3-662-53401-4

Copyright Year: 2016

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

Premium Partner

    Image Credits