Skip to main content
SpringerLink
Log in

A Coloured Petri Net Approach to Protocol Verification

  • Chapter
Lectures on Concurrency and Petri Nets (ACPN 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3098))

Included in the following conference series:

Abstract

The correct operation of communication and co-operation protocols, including signalling systems in various networks, is essential for the reliability of the many distributed systems that facilitate our global economy. This paper presents a methodology for the formal specification, analysis and verification of protocols based on the use of Coloured Petri nets and automata theory. The methodology is illustrated using two case studies. The first belongs to the category of data transfer protocols, called Stop-and-Wait Protocols, while the second investigates the connection management part of the Internet’s Transmission Control Protocol (TCP). Stop-and-Wait protocols (SWP) incorporate retransmission strategies to recover from data transmission errors that occur on noisy transmission media. Although relatively simple, their basic mechanisms are important for practical protocols such as the data transfer procedures of TCP. The SWP case study is quite detailed. It considers a class of protocols characterized by two parameters: the maximum sequence number (MaxSeqNo) and the maximum number of retransmissions (MaxRetrans). We investigate the operation of the protocol over (lossy) in-sequence (FIFO) channels, and then over (lossy) re-ordering media, such as that provided by the Internet Protocol. Four properties are considered: the bound on the number of messages that can be in the communication channels; whether or not the protocol provides the expected service of alternating sends and receives; (unknowing) loss of messages (i.e. data sent but not received, and not detected as lost by the protocol); and the acceptance of duplicates as new messages. The model is analysed using a combination of hand proofs and automatic techniques. A new result for the bound of the channels (2MaxRetrans+1) is proved for FIFO channels. It is further shown that for re-ordering channels, the channels are unbounded, loss and duplication can occur, and that the SWP does not provide the expected service. We discuss the relevance of these results to the Transmission Control Protocol and indicate the limitations of our approach and the need for further work. The second case study (TCP) illustrates the use of hierarchies to provide a compact and readable CPN model for a complex protocol. We advocate an incremental approach to both modelling and analysis. The importance of stating the assumptions involved is emphasised and we illustrate how they affect the abstractions that can be made to simplify the model. The incremental approach to analysis allows us to validate the model against the TCP definition and to show how errors in the connection establishment procedures can be found. Finally we provide some observations and tips on the how the methodology can be used based on many years of experience. The emphasis of the paper is on providing a tutorial style introduction to the methodology, examining case studies in depth, rather than breadth, and giving some insight into the process while noting its limitations.

Partially supported by an Australian Research Council (ARC) Discovery Grant (DP0210524).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aziz Abdulla, P., Jonsson, B.: Verifying Programs with Unreliable Channels. Information and Computation 127(2), 91–101 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  2. Afek, Y., Attiya, H., Fekete, A., Fischer, M., Lynch, N., Mansour, Y., Wang, D., Zuck, L.: Reliable Communication Over Unreliable Channels. Journal of the ACM 41(6), 1267–1297 (1994)

    Article  MathSciNet  Google Scholar 

  3. Afek, Y., Brown, G.M.: Self-Stabilization of the Alternating Bit Protocol. In: Proceedings of the 8th Symposium on Reliable Distributed Systems, pp. 80–83. IEEE Comput. Soc. Press, Los Alamitos (1989)

    Chapter  Google Scholar 

  4. Babich, F., Deotto, L.: Formal Methods for the Specification and Analysis of Communication Protocols. IEEE Communications Surveys 4(1), 2–20 (Third Quarter 2002)

    Article  Google Scholar 

  5. Barrett, W.A., Couch, J.D.: Compiler Construction: Theory and Practice. Science Research Associates (1979)

    Google Scholar 

  6. Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A Note on Reliable Full-Duplex Transmission over Half-Duplex Links. Communications of the ACM 12(5), 260–261 (1969)

    Article  Google Scholar 

  7. Billington, J.: Abstract Specification of the ISO Transport Service Definition using Labelled Numerical Petri Nets. Protocol Specification, Testing, and Verification, vol. III, pp. 173–185. Elsevier Science Publishers, Amsterdam (1983)

    Google Scholar 

  8. Billington, J.: Extensions to Coloured Petri Nets. In: Petri Nets and Performance Models, The Proceedings of the Third International Workshop, PNPM 1989, Kyoto, Japan, December 11-13, pp. 61–70. IEEE Computer Society, Los Alamitos (1989)

    Google Scholar 

  9. Billington, J.: Formal specification of protocols: Protocol Engineering. In: Encyclopedia of Microcomputers, vol. 7, pp. 299–314. Marcel Dekker, New York (1991)

    Google Scholar 

  10. Billington, J.: Protocol Specification using P-Graphs, a Technique based on Coloured Petri Nets. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1492, pp. 293–330. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. Billington, J., Díaz, M., Rozenberg, G. (eds.): APN 1999. LNCS, vol. 1605. Springer, Heidelberg (1999)

    Google Scholar 

  12. Billington, J., Gallasch, G.E.: How Stop and Wait Protocols Can Fail Over The Internet. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 209–223. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Billington, J., Gallasch, G.E.: An Investigation of the Properties of Stop-and-Wait Protocols over Channels which can Re-order messages. Technical Report 15, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Australia (2004)

    Google Scholar 

  14. Billington, J., Gallasch, G.E., 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–37 (2004)

    Article  Google Scholar 

  15. Billington, J., Han, B.: Formalising the TCP Symmetrical Connection Management Service. In: Proceedings of the Design, Analysis and Simulation of Distributed Systems Conference, Orlando, Florida, USA, March 2003, pp. 178–184 (2003)

    Google Scholar 

  16. Billington, J., Han, B.: On Defining the Service Provided by TCP. In: Proceedings of the 26th Australasian Computer Science Conference, Adelaide, Australia, February 2003. Conferences in Research and Practice in Information Technology, vol. 16, pp. 129–138 (2003)

    Google Scholar 

  17. Billington, J., Han, B.: Closed Form Expressions for the State Space of TCP’s Data Transfer Service Operating over Unbounded Channels. In: Proceedings of the 27th Australasian Computer Science Conference, Dunedin, New Zealand, January 2004. Conferences in Research and Practice in Information Technology, vol. 26, pp. 31–39 (2004)

    Google Scholar 

  18. Billington, J., Wheeler, G.R., Wilbur-Ham, M.C.: PROTEAN: A High-level Petri Net Tool for the Specification and Verification of Communication Protocols. IEEE Transactions on Software Engineering 14(3), 301–316 (1988)

    Article  Google Scholar 

  19. Billington, J., Wilbur-Ham, M.C., Bearman, M.Y.: Automated Protocol Verification. In: Protocol Specification, Testing and Verification, V, pp. 59–70. North Holland, Amsterdam (1986)

    Google Scholar 

  20. Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Comput. Networks and ISDN Sys. 14(1), 25–59 (1987)

    Article  Google Scholar 

  21. Budkowski, S., Dembinski, P.: An Introduction to Estelle: A Specification Language for Distributed Systems. Comput. Networks and ISDN Sys. 14(1), 3–23 (1987)

    Article  Google Scholar 

  22. CCITT. ISDN user-network interface data link layer specification. Technical report, Draft Recommendation Q.921, Working Party XI/6, Issue 7 (January 1984)

    Google Scholar 

  23. Christensen, S., Jepsen, L.O.: Modelling and Simulation of a Network Management System Using Hierarhical Coloured Petri Nets. In: Proceedings of the 1991 European Simulation Multiconference, Society for Computer Simulation, pp. 47–52 (1991)

    Google Scholar 

  24. Christensen, S., Jørgensen, J.B.: Analysis of Bang and Olufsen’s BeoLink Audio/Video System Using Coloured Petri Nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 387–406. Springer, Heidelberg (1997)

    Google Scholar 

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

  26. Comer, D.E.: Internetworking with TCP/IP: Principles, Protocols, and Architecture, vol. 1. Prentice Hall, Upper Saddle River (2000)

    Google Scholar 

  27. CPN ML: An Extension of Standard ML, http://www.daimi.au.dk/designCPN/sml/cpnml.html

  28. Desel, J., Reisig, W.: Place/Transition Petri Nets. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 122–173. Springer, Heidelberg (1998)

    Google Scholar 

  29. Design/CPN Online, http://www.daimi.au.dk/designCPN/

  30. Diaz, M.: Modelling and Analysis of Communication and Co-operation Protocols Using Petri Net Based Models. In: Protocol Specification, Testing and Verification, pp. 465–510. North-Holland, Amsterdam (1982)

    Google Scholar 

  31. Fone, G.A.: Modelling ISDN Supplementary Services Using Coloured Petri Nets. In: Proceedings of Communications 1992, Sydney, Australia, pp. 37–41 (1992)

    Google Scholar 

  32. Floreani, D.J., Billington, J., Dade, A.: Designing and Verifying a Communications Gateway Using Colored Petri Nets and Design/CPN. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 153–171. Springer, Heidelberg (1996)

    Google Scholar 

  33. FSM Library, AT&T Research Labs, http://www.research.att.com/sw/tools/fsm/

  34. Gordon, S.: Verification of the WAP Transaction Layer using Coloured Petri Nets. PhD thesis, School of Electrical and Information Engineering, University of South Australia (2001)

    Google Scholar 

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

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

  37. Han, B.: Formal Specification of the TCP Service and Verification of TCP Connection Management. Draft PhD Thesis, University of South Australia (April 2004)

    Google Scholar 

  38. Han, B., Billington, J.: An Analysis of TCP Connection Management Using Coloured Petri Nets. In: Proceedings of the 5th World Multi-Conference on Systemics, Cybernetics and Informatics (SCI 2001), Orlando, Florida, July 2001, pp. 590–595 (2001)

    Google Scholar 

  39. Han, B., Billington, J.: Validating TCP Connection Management. In: Proceedings of the Workshop on Software Engineering and Formal Methods, Adelaide, Australia, June 2002. Conferences in Research and Practice in Information Technology, vol. 12, pp. 47–55 (2002)

    Google Scholar 

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

    Google Scholar 

  41. International Telecommunication Union, http://www.itu.int/home/

  42. Internet Engineering Task Force, http://www.ietf.org

  43. The Internet Engineering Task Force. TCP Extensions for High Performance. RFC 1323 (1992)

    Google Scholar 

  44. ISO/IEC FDIS 15909-1, Final Draft International Standard, International Organisation for Standardization (February 2004)

    Google Scholar 

  45. ITU-T. Recommendation Z.100: Functional Specification and Description Language (SDL). International Telecommunications Union (2002)

    Google Scholar 

  46. ITU-T. Recommendation X.210, Information Technology - Open Systems Interconnection - Basic Reference Model: Conventions for the Definition of OSI Services. International Telecommunications Union (November 1993)

    Google Scholar 

  47. Jensen, K.: Coloured Petri Nets and the Invariant Method. Theoretical Computer Science 14, 317–336 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  48. Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, 2nd edn. Basic Concepts, vol. 1. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  49. Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, 2nd edn. Analysis Methods, vol. 2. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  50. Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use. Practical Use, vol. 3. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  51. Jørgensen, J.B., Mortensen, K.H.: Modelling and Analysis of Distributed Program Execution in BETA Using Coloured Petri Nets. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 249–268. Springer, Heidelberg (1996)

    Google Scholar 

  52. Knuth, D.E.: Verification of Link-Level Protocols. BIT 21, 31–36 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  53. Kristensen, L.M., Christensen, S., Jensen, K.: The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer 2(2), 98–132 (1998)

    Article  MATH  Google Scholar 

  54. Lazic, R., Nowak, D.: A Unifying Approach to Data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 581–595. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  55. Liu, L., Billington, J.: Modelling and Analysis of the CES Protocol of H.245. In: Proc. of the Third Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Aarhus, Denmark, August 2001, pp. 29–31 (2001)

    Google Scholar 

  56. Liu, L., Billington, J.: Tackling the Infinite State Space of a Multimedia Control Protocol Service Specification. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 273–293. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  57. Liu, L., Billington, J.: Obtaining the Service Language for H.245’s Multimedia Capability Exchange Signalling Protocol: the Final Step. In: Proc. of the 10th International Multi-Media Modelling Conference, Brisbane, Australia, January 5-7 (2004)

    Google Scholar 

  58. Ouyang, C.: Formal Specification and Verification of the Internet Open Trading Protocol using Coloured Petri Nets.PhD thesis, School of Electrical and Information Engineering, University of South Australia, Australia (March 2004) (submitted)

    Google Scholar 

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

  60. Ouyang, C., Kristensen, L.M., Billington, J.: A formal service specification of 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 

  61. Postel, J.: Internet Protocol - DARPA Internet Program Protocol Specification. RFC 791, IETF (September 1981)

    Google Scholar 

  62. Postel, J.: Transmission Control Protocol. RFC 793 (1981)

    Google Scholar 

  63. Reisig, W.: Elements of Distributed Algorithms: Modelling and Analysis with Petri Nets. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  64. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall International Series in Computer Science (1998)

    Google Scholar 

  65. Sabnani, K.: An Algorithmic Technique for Protocol Verification. IEEE Transactions on Communications 36(8), 924–931 (1988)

    Article  MATH  Google Scholar 

  66. Stallings, W.: Data and Computer Communications, 6th edn. Prentice Hall, Englewood Cliffs (2000)

    Google Scholar 

  67. Standard ML of New Jersey, http://cm.bell-labs.com/cm/cs/what/smlnj/

  68. Steggles, L.J., Kosiuczenko, P.: A Timed Rewriting Logic Semantics for SDL: a case study of the Alternating Bit Protocol. Electronic Notes in Theoretical Computer Science 15 (1998)

    Google Scholar 

  69. Stevens, W.R.: TCP/IP Illustrated, vol. 1. Addison-Wesley, Reading (1994)

    MATH  Google Scholar 

  70. Sunshine, C.A.: Formal Techniques for Protocol Specification and Verification. IEEE Computer, 346-350 (September 1979)

    Google Scholar 

  71. Suzuki, I.: Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets. IEEE Transactions on Software Engineering 16(11), 1273–1281 (1990)

    Article  Google Scholar 

  72. Suzuki, I.: Specification and Verification of the Alternating Bit Protocol by Temporal Petri Nets. In: Proceedings of the 32nd Midwest Symposium on Circuits and Systems, pp. 157–160. IEEE Press, Los Alamitos (1990)

    Chapter  Google Scholar 

  73. Tanenbaum, A.: Computer Networks, 4th edn. Prentice Hall, Englewood Cliffs (2003)

    Google Scholar 

  74. Tokmakoff, A., Billington, J.: An Approach to the Analysis of Interworking Traders. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 127–146. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  75. Tomlinson, R.S.: Selecting sequence numbers. In: Proc. of SIGCOMM/SIGOPS Interprocess Commun. Workshop, pp. 11–23. ACM, New York (1975)

    Chapter  Google Scholar 

  76. Turner, K.J. (ed.): Using Formal Description Techniques: An Introduction to Estelle, Lotos and SDL. Wiley Series in Communication and Distributed Systems. John Wiley & Sons, Chichester (1993)

    Google Scholar 

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

    Google Scholar 

  78. Villapol, M.E.: Modelling and Analysis of the Resource Reservation Protocol. PhD thesis, Electrical and Information Engineering, University of South Australia, Australia (November 2003)

    Google Scholar 

  79. Villapol, M.E., Billington, J.: Generation of a Service Language for the Resource Reservation Protocol using Formal Methods. In: Proc. INCOSE 2001, the 11th Annual International Symposium of the International Council on Systems Engineering, July 1-5, CD-ROM, Melbourne, Australia (2001)

    Google Scholar 

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

  81. WAP Forum, http://www.wapforum.org/

  82. Wolper, P.: Expressing Interesting Properties of Programs in Propositional Temporal Logic. In: Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 184–193. ACM, New York (1986)

    Google Scholar 

  83. Xu, J., Kuusela, J.: Analyzing the Execution Architecture of Mobile Phone Software with Coloured Petri Nets. Int. Journal on Software Tools for Technology Transfer 2(2), 133–143 (1998)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Systems Engineering Centre, University of South Australia, Mawson Lakes Campus, SA, 5095, Australia

    Jonathan Billington, Guy Edward Gallasch & Bing Han

Authors
  1. Jonathan Billington
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Guy Edward Gallasch
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bing Han
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Applied Computer Science, Catholic University of Eichstätt-Ingolstadt,  

    Jörg Desel

  2. Institut für Informatik, Humboldt-Universität zu Berlin, Unter den Linden 6, 10099, Berlin, Germany

    Wolfgang Reisig

  3. , Leiden Center of Advanced Computer Science (LIACS), Leiden University, Niels Bohrweg 1, 2333, Leiden, CA, The Netherlands

    Grzegorz Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Billington, J., Gallasch, G.E., Han, B. (2004). A Coloured Petri Net Approach to Protocol Verification. In: Desel, J., Reisig, W., Rozenberg, G. (eds) Lectures on Concurrency and Petri Nets. ACPN 2003. Lecture Notes in Computer Science, vol 3098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27755-2_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27755-2_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22261-3

  • Online ISBN: 978-3-540-27755-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation