[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Applications of Coloured Petri Nets for Functional Validation of Protocol Designs

  • Conference paper
Transactions on Petri Nets and Other Models of Concurrency VII

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

Abstract

Communication protocols constitute central building blocks in most modern IT systems as they define components, rules, and languages that make data communication possible. The development of correct protocols is a challenging engineering discipline, making modelling and validation of protocol design an important application domain for Coloured Petri Nets (CPNs). We illustrate the practical application of CPNs for protocol validation by focusing on selected aspects of four recent projects involving industrial-sized protocols. These projects demonstrate how CPNs can be used to model protocol elements and improve protocol specifications, how state space exploration can be used to verify protocol properties, and how behavioural visualisation in combination with a CPN model provides an effective way of rapidly constructing an executable prototype of a protocol design.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. ISO/IEC 15437. Information technology. Enhancements to LOTOS (E-LOTOS) (September 2001)

    Google Scholar 

  2. 3GPP. Digital Cellular Telecommunications System (Phase 2+); Generic Access to the A/Gb Interface; Stage 2. 3GPP TS 43.318 version 6.9.0 Release 6 (March 2007)

    Google Scholar 

  3. 3GPP. Website of 3GPP (May 2007), http://www.3gpp.org

  4. Alur, R., Holzmann, G., Peled, D.: An analyzer for message sequence charts. Software - Concepts and Tools 17(2), 70–77 (1996)

    Google Scholar 

  5. Ardis, M.A.: Formal Methods for Telecommunication System Requirements: A Survey of Standardised Languages. Annals of Software Engineering 3 (1997)

    Google Scholar 

  6. Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press (2008)

    Google Scholar 

  7. Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Billington, J., Gallasch, G., Kristensen, L.M., Mailund, T.: Exploiting Equivalence Reduction and the Sweep-Line Method for Detecting Terminal States. IEEE Transactions on Systems, Man, and Cybernetics. Part A: Systems and Humans 34(1), 23–38 (2004)

    Article  Google Scholar 

  9. 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 

  10. Billington, J., Han, B.: Modelling and Analysing the Functional Behaviour of TCPs Connection Management Procedures. International Journal on Software Tools for Technology Transfer 9(3-4), 269–304 (2007)

    Article  Google Scholar 

  11. Billington, J., Vanit-Anunchai, S.: Coloured Petri Net Modelling of an Evolving Internet Protocol Standard: The Datagram Congestion Control Protocol. Fundamenta Informaticae 88(3), 357–385 (2008)

    MathSciNet  MATH  Google Scholar 

  12. Billington, J., Yuan, C.: On Modelling and Analysing the Dynamic MANET On-Demand (DYMO) Routing Protocol. In: Jensen, K., Billington, J., Koutny, M. (eds.) Transactions on Petri Nets and Other Models of Concurrency III. LNCS, vol. 5800, pp. 98–126. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. Bochmann, G.: Finite state description of protocols. Computer Networks, 361–372 (1978)

    Google Scholar 

  14. Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks 14, 25–59 (1987)

    Google Scholar 

  15. Chakeres, I.D., Perkins, C.E.: Dynamic MANET On-demand (DYMO) Routing. Internet-Draft. Work in Progress (July 2007), http://www.ietf.org/internet-drafts/draft-ietf-manet-dymo-10.txt

  16. Chakeres, I.D., Perkins, C.E.: Dynamic MANET On-demand (DYMO) Routing. Internet-Draft. Work in Progress (November 2007), http://www.ietf.org/internet-drafts/draft-ietf-manet-dymo-11.txt

  17. Choppy, C., Dedova, A., Evangelista, S., Hong, S., Klai, K., Petrucci, L.: The NEO Protocol for Large-Scale Distributed Database Systems: Modelling and Initial Verification. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 145–164. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Choppy, C., Petrucci, L., Reggio, G.: A Modelling Approach with Coloured Petri Nets. In: Kordon, F., Vardanega, T. (eds.) Ada-Europe 2008. LNCS, vol. 5026, pp. 73–86. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  20. Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting Symmetries in Temporal Logic Model Checking. Formal Methods in System Design 9, 77–104 (1996)

    Article  Google Scholar 

  21. Comer, D.E.: Internetworking with TCP/IP vol. 1: Principles, Protocols, and Architecture, 5th edn. Prentice-Hall (2005)

    Google Scholar 

  22. Deering, S., Hinden, R.: Internet Protocol, Version 6 (IPV6) Specification. RFC 2460 (December 1998)

    Google Scholar 

  23. Ding, L.G., Liu, L.: Modelling and Analysis of the INVITE Transaction of the Session Initiation Protocol Using Coloured Petri Nets. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 132–151. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  24. Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. Formal Methods in System Design 9, 105–131 (1996)

    Article  Google Scholar 

  25. Espensen, K.L., Kjeldsen, M.K., Kristensen, L.M.: Modelling and Initial Validation of the DYMO Routing Protocol for Mobile Ad-Hoc Networks. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 152–170. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  26. ETSI. ETSI ES 201 873-1: Methods for Testing and Specification; The Testing and Test Control Notation version 3; Part 1: TTCN-3 Core Language

    Google Scholar 

  27. Evangelista, S., Westergaard, M., Kristensen, L.M.: The ComBack Method Revisited: Caching Strategies and Extension with Delayed Duplicate Detection. Transactions on Petri Nets and Other Models of Concurrency 3, 189–215 (2009)

    Article  Google Scholar 

  28. Examples of Industrial Use of CPNs, http://cs.au.dk/cpnets/industrial-use/

  29. Fehnker, A., van Glabbeek, R., Hofner, P., McIver, A., Portmann, M., Tan, W.: Modelling and Analysis of AODV in UPPAAL. In: Proc. of 1st Workshop on Rigorous Protocol Engineering (2011)

    Google Scholar 

  30. Fleischer, P., Kristensen, L.M.: Modelling and Validation of Secure Connection Establishment in a Generic Access Network Scenario. Fundamenta Informaticae 94(3-4), 361–386 (2009)

    MathSciNet  Google Scholar 

  31. Gallasch, G.E., Billington, J.: Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 457–473. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  32. Gallasch, G.E., Billington, J.: A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 201–218. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  33. Gallasch, G.E., Billington, J., Vanit-Anunchai, S., Kristensen, L.M.: Checking Safety Properties On-the-fly with the Sweep-Line Method. International Journal on Software Tools for Technology Transfer (STTT) 9(3-4), 371–392 (2007)

    Article  Google Scholar 

  34. Gallasch, G.E., Ouyang, C., Billington, J., Kristensen, L.M.: Experimenting with Progress Mappings for the Sweep-Line Analysis of the Internet Open Trading Protocol. In: Proc. of 5th Workshop and Tutorial on Practical Use of Coloured Petri Nets and CPN Tools (CPN 2004), pp. 19–38 (2004)

    Google Scholar 

  35. Gallasch, G.E., Han, B., Billington, J.: Sweep-Line Analysis of TCP Connection Management. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 156–172. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  36. Gehlot, V., Hayrapetyan, A.: A Formalized and Validated Executable Model of the SIP-based Presence Protocol for Mobile Applications. In: Proceedings of the 45th Annual ACM Southeast Regional Conference, pp. 185–190. ACM (2007)

    Google Scholar 

  37. Gehlot, V., Hayrapetyan, A.: A CPN Model of a SIP-Based Dynamic Discovery Protocol for Webservices in a Mobile Environment. In: Proc. of 7th Workshop and Tutorial onPractical Use of Coloured Petri Nets and the CPN Tools, CPN 2006 (2006)

    Google Scholar 

  38. Genest, B., Muscholl, A., Peled, D.: Message sequence charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 537–558. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  39. Gordon, S.: Formal Analysis of PANA Authentication and Authorisation Protocol. In: Proc. of 9th International Conference on Parallel and Distributed Computing, Applications and Technologies, pp. 277–284. IEEE Computer Society (2008)

    Google Scholar 

  40. Gordon, S., Billington, J.: Analysing the WAP Class 2 Wireless Transaction Protocol Using Coloured Petri Nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 207–226. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  42. Grimstrup, P.: Interworking Description for IKEv2 Library. In: Ericsson Internal. Document No. 155 10-FCP 101 4328 Uen (September 2006)

    Google Scholar 

  43. Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8(3), 231–274 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  44. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985)

    Google Scholar 

  45. Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley (2004)

    Google Scholar 

  46. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall (1991)

    Google Scholar 

  47. The Internet Engineering Task Force (IETF), http://www.ietf.org

  48. Ip, C.N., Dill, D.L.: Better Verification Through Symmetry. Formal Methods in System Design 9, 41–75 (1996)

    Article  Google Scholar 

  49. ISO9074. Information Processing Systems - Open Systems Interconnection: ESTELLE (FOrmal Description Technique Based on an Extended State Transition Model)

    Google Scholar 

  50. ISO89 ISO/IEC. Information Processing Systems - Open Systems Interconnection: LOTOS, a Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. IS 8807 (February 1989)

    Google Scholar 

  51. ITU-T. Z.120: Message Sequence Charts (MSC) (1996)

    Google Scholar 

  52. ITU-T. Z.109: SDL-2000 Combined with UML (2000)

    Google Scholar 

  53. ITU-T. X.680 to X.683: Abstract Syntax Notation One (2002)

    Google Scholar 

  54. ITU-T. X.692 - Encoding Control Notation (2002)

    Google Scholar 

  55. ITU-T. Z.100-Z.106: Specification and Description Language (SDL) (2010)

    Google Scholar 

  56. Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. vol. 1: Basic Concepts. Monographs in Theoretical Computer Science. Springer (1992)

    Google Scholar 

  57. Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Analysis Methods. Monographs in Theoretical Computer Science, vol. 2. Springer (1994)

    Google Scholar 

  58. Jensen, K.: Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design 9, 7–40 (1996)

    Article  Google Scholar 

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

    Google Scholar 

  60. Jensen, K., Kristensen, L.M., Mailund, T.: The sweep-line state space exploration method. Theoretical Computer Science 429, 169–179 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  61. Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. International Journal on Software Tools for Technology Transfer (STTT) 9(3-4), 213–254 (2007)

    Article  Google Scholar 

  62. Jørgensen, J.B., Kristensen, L.M.: Computer Aided Verification of Lamport’s Fast Mutual Exclusion Algorithm Using Coloured Petri Nets and Occurrence Graphs with Symmetries. IEEE Transactions on Parallel and Distributed Systems 10(7), 714–732 (1999)

    Article  Google Scholar 

  63. Jørgensen, J.B., Kristensen, L.M.: Verification of Coloured Petri Nets Using State Spaces with Equivalence Classes. In: Petri Net Approaches for Modelling and Validation, Lincoln Europa. LINCOM Studies in Computer Science, ch. 2, vol. 1, pp. 17–34 (2003)

    Google Scholar 

  64. Kaufman, C.: Internet Key Exchange Protocol. RFC 4306 (December 2005)

    Google Scholar 

  65. Kent, S., Seo, K.: Security Architecture for the Internet Protocol. RFC 4301 (December 2005)

    Google Scholar 

  66. Kristensen, L.M.: A Perspective on Explicit State Space Exploration of Coloured Petri Nets: Past, Present, and Future. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 39–42. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  67. Kristensen, L.M., Jensen, K.: Specification and Validation of an Edge Router Discovery Protocol for Mobile Ad Hoc Networks. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 248–269. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  68. 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 

  69. Kristensen, L.M., Mailund, T.: Efficient Path Finding with the Sweep-Line Method Using External Storage. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 319–337. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  70. Kristensen, L.M., Mechlenborg, P., Zhang, L., Mitchell, B., Gallasch, G.E.: Model-based Development of COAST. STTT 10(1), 5–14 (2007)

    Article  Google Scholar 

  71. 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.) ACPN. LNCS, vol. 3098, pp. 626–685. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  72. Kristensen, L.M., Valmari, A.: Finding Stubborn Sets of Coloured Petri Nets Without Unfolding. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, pp. 104–123. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  73. Kristensen, L.M., Westergaard, M.: Automatic Structure-Based Code Generation from Coloured Petri Nets: A Proof of Concept. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 215–230. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  74. Kristensen, L.M., Westergaard, M., Nørgaard, P.C.: Model-Based Prototyping of an Interoperability Protocol for Mobile Ad-Hoc Networks. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 266–286. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  75. Lai, R., Jirachiefpattana, A.: Communication Protocol Specification and Verification. Kluwer Academic Publishers (1998)

    Google Scholar 

  76. Lakos, C.: Modelling Mobile IP with Mobile Petri Nets. Transactions on Petri Nets and Other Models of Concurrency 5800, 127–158 (2009)

    Article  Google Scholar 

  77. Liu, L.: Verification of the SIP Transaction Using Coloured Petri Nets. In: Mans, B. (ed.) Thirty-Second Australasian Computer Science Conference (ACSC 2009), Wellington, New Zealand. CRPIT, vol. 91, pp. 63–72. ACS (2009)

    Google Scholar 

  78. Liu, L.: Security Analysis of Session Initiation Protocol - A Methodology Based on Coloured Petri Nets. In: Proc. of the 2010 International Cyber Resilience Conference (2010)

    Google Scholar 

  79. Liu, L., Billington, J.: Verification of the Capability Exchange Signalling protocol. STTT 9(3-4), 305–326 (2007)

    Article  Google Scholar 

  80. Liu, M.T.: Protocol Engineering. Advances in Computers 29, 79–195 (1989)

    Article  Google Scholar 

  81. Lorentsen, L., Kristensen, L.M.: Modelling and Analysis of a Danfoss Flowmeter System Using Coloured Petri Nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 346–366. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  82. IETF Mobile Ad-hoc Networks Discussion Archive, http://www1.ietf.org/mail-archive/web/manet/current/index.html

  83. Mailund, T.: Analysing infinite-state systems by combining equivalence reduction and the sweep-line method. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 314–333. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  84. Malik, R., Mühlfeld, R.: A case study in verification of uml statecharts: the profisafe protocol. Universal Computer Science 9(2), 138–151 (2003)

    Google Scholar 

  85. Malkin, G.: RIP Version 2. RFC 4822 (February 2007)

    Google Scholar 

  86. Milner, R.: Communication and Concurrency. Prentice-Hall International (1989)

    Google Scholar 

  87. Mortensen, K.H.: Automatic Code Generation Method Based on Coloured Petri Net Models Applied on an Access Control System. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 367–386. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  88. Narten, T., Nordmark, E., Simpson, W.: Neighbor Discovery for IP Version 6 (IPv6), RFC 2461 (December 1998)

    Google Scholar 

  89. Ouyang, C., Billington, J.: On Verifying the Internet Open Trading Protocol. In: Bauknecht, K., Tjoa, A.M., Quirchmayr, G. (eds.) EC-Web 2003. LNCS, vol. 2738, pp. 292–302. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  90. Ouyang, C., Billington, J.: Formal Analysis of the Internet Open Trading Protocol. In: Núñez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol. 3236, pp. 1–15. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  91. Ouyang, C., Kristensen, L.M., Billington, J.: A Formal and Executable Specification of the Internet Open Trading Protocol. In: Bauknecht, K., Tjoa, A.M., Quirchmayr, G. (eds.) EC-Web 2002. LNCS, vol. 2455, pp. 377–387. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  92. Ouyang, C., Kristensen, L.M., Billington, J.: A Formal Service Specification for the Internet Open Trading Protocol. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 352–373. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  93. Petri, C.A.: Kommunikation mit Automaten. Bonn: Institut für Instrumentelle Mathematik, Schriften des IIM Nr. 2 (1962)

    Google Scholar 

  94. Popovic, M.: Communication Protocol Engineering. CRC Press (2006)

    Google Scholar 

  95. Ratzer, A.V., Wells, L., Lassen, H.M., Laursen, M., Qvortrup, J.F., Stissing, M.S., Westergaard, M., Christensen, S., Jensen, K.: CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 450–462. Springer, Heidelberg (2003), http://www.cpntools.org

    Chapter  Google Scholar 

  96. Ravn, A.P., Srba, J., Vighio, S.: Modelling and verification of web services business activity protocol. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 357–371. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  97. Reisig, W.: Petri Nets - An Introduction. EATCS Monographs on Theoretical Computer Science, vol. 4. Springer (1985)

    Google Scholar 

  98. Stern, U., Dill, D.L.: Improved Probabilistic Verification by Hash Compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 206–224. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  99. Suriadi, S., Ouyang, C., Smith, J., Foo, E.: Modeling and Verification of Privacy Enhancing Protocols. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 127–146. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  100. Ullman, J.D.: Elements of ML Programming. Prentice-Hall (1998)

    Google Scholar 

  101. Valmari, A.: A Stubborn Attack on State Explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  102. Valmari, A.: Stubborn Sets of Coloured Petri Nets. In: Proc. of ICATPN 1991, pp. 102–121 (1991)

    Google Scholar 

  103. Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  104. Vanit-Anunchai, S.: Towards Formal Modelling and Analysis of SCTP Connection Management. In: Proc. of CPN 2009, pp. 163–182 (2008)

    Google Scholar 

  105. Vanit-Anunchai, S., Billington, J., Gallasch, G.E.: Analysis of the Datagram Congestion Control Protocols Connection Management Procedures Using the Sweep-line Method. International Journal on Software Tools for Technology Transfer 10(1), 29–56 (2008)

    Article  Google Scholar 

  106. Villapol, M.E., Billington, J.: A Coloured Petri Net Approach to Formalising and Analysing the Resource Reservation Protocol. CLEI Electron. J. 6(1) (2003)

    Google Scholar 

  107. Villapol, M.E., Billington, J.: Analysing Properties of the Resource Reservation Protocol. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 377–396. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  108. Vixie, P.: Dynamic Updates in the Domain Name System. RFC 2136 (April 1997)

    Google Scholar 

  109. Westergaard, M., Evangelista, S., Kristensen, L.M.: ASAP: An Extensible Platform for State Space Analysis. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 303–312. Springer, Heidelberg (2009), http://www.daimi.au.dk/~ascoveco/download.html

    Chapter  Google Scholar 

  110. Westergaard, M., Kristensen, L.M., Brodal, G.S., Arge, L.A.: The ComBack Method – Extending Hash Compaction with Backtracking. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 445–464. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  111. Westergaard, M., Lassen, K.B.: The BRITNeY Suite Animation Tool. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 431–440. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  112. Westergaard, M.: A Game-theoretic Approach to Behavioural Visualisation. Electr. Notes Theor. Comput. Sci. 208, 113–129 (2008)

    Article  Google Scholar 

  113. Wolper, P., Leroy, D.: Reliable Hashing without Collision Detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 59–70. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Engineering, Bergen University College, Norway

    Lars M. Kristensen & Kent Inge Fagerland Simonsen

  2. DTU Informatics, Technical University of Denmark, Denmark

    Kent Inge Fagerland Simonsen

Authors
  1. Lars M. Kristensen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kent Inge Fagerland Simonsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Science, Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, 8200, Aarhus N, Denmark

    Kurt Jensen

  2. Department of Information Systems, Eindhoven University of Technology, P.O. Box 513, NL-5600, Eindhoven, MB, The Netherlands

    Wil M. P. van der Aalst

  3. Dipartimento di Informatica, Università degli Studi di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Gianfranco Balbo

  4. School of Computing Science, Newcastle University, Newcastle upon Tyne, UK

    Maciej Koutny

  5. Institut für Informatik, Universität Rostock, Germany

    Karsten Wolf

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kristensen, L.M., Simonsen, K.I.F. (2013). Applications of Coloured Petri Nets for Functional Validation of Protocol Designs. In: Jensen, K., van der Aalst, W.M.P., Balbo, G., Koutny, M., Wolf, K. (eds) Transactions on Petri Nets and Other Models of Concurrency VII. Lecture Notes in Computer Science, vol 7480. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38143-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38143-0_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38142-3

  • Online ISBN: 978-3-642-38143-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation