Advertisement

A Coloured Petri Net Approach to Protocol Verification

  • Jonathan Billington
  • Guy Edward Gallasch
  • Bing Han
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3098)

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.

Keywords

Transmission Control Protocol Finite State Automaton Reachability Graph Protocol Entity Retransmission Counter 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aziz Abdulla, P., Jonsson, B.: Verifying Programs with Unreliable Channels. Information and Computation 127(2), 91–101 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 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)CrossRefMathSciNetGoogle Scholar
  3. 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)CrossRefGoogle Scholar
  4. 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)CrossRefGoogle Scholar
  5. 5.
    Barrett, W.A., Couch, J.D.: Compiler Construction: Theory and Practice. Science Research Associates (1979)Google Scholar
  6. 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)CrossRefGoogle Scholar
  7. 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. 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. 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. 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)CrossRefGoogle Scholar
  11. 11.
    Billington, J., Díaz, M., Rozenberg, G. (eds.): APN 1999. LNCS, vol. 1605. Springer, Heidelberg (1999)Google Scholar
  12. 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)CrossRefGoogle Scholar
  13. 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. 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)CrossRefGoogle Scholar
  15. 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. 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. 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. 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)CrossRefGoogle Scholar
  19. 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. 20.
    Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Comput. Networks and ISDN Sys. 14(1), 25–59 (1987)CrossRefGoogle Scholar
  21. 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)CrossRefGoogle Scholar
  22. 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. 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. 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. 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)CrossRefGoogle Scholar
  26. 26.
    Comer, D.E.: Internetworking with TCP/IP: Principles, Protocols, and Architecture, vol. 1. Prentice Hall, Upper Saddle River (2000)Google Scholar
  27. 27.
    CPN ML: An Extension of Standard ML, http://www.daimi.au.dk/designCPN/sml/cpnml.html
  28. 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. 29.
  30. 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. 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. 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. 33.
    FSM Library, AT&T Research Labs, http://www.research.att.com/sw/tools/fsm/
  34. 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. 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)CrossRefGoogle Scholar
  36. 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)CrossRefGoogle Scholar
  37. 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. 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. 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. 40.
    Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)Google Scholar
  41. 41.
    International Telecommunication Union, http://www.itu.int/home/
  42. 42.
    Internet Engineering Task Force, http://www.ietf.org
  43. 43.
    The Internet Engineering Task Force. TCP Extensions for High Performance. RFC 1323 (1992)Google Scholar
  44. 44.
    ISO/IEC FDIS 15909-1, Final Draft International Standard, International Organisation for Standardization (February 2004)Google Scholar
  45. 45.
    ITU-T. Recommendation Z.100: Functional Specification and Description Language (SDL). International Telecommunications Union (2002)Google Scholar
  46. 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. 47.
    Jensen, K.: Coloured Petri Nets and the Invariant Method. Theoretical Computer Science 14, 317–336 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  48. 48.
    Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, 2nd edn. Basic Concepts, vol. 1. Springer, Heidelberg (1997)zbMATHGoogle Scholar
  49. 49.
    Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, 2nd edn. Analysis Methods, vol. 2. Springer, Heidelberg (1997)zbMATHGoogle Scholar
  50. 50.
    Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use. Practical Use, vol. 3. Springer, Heidelberg (1997)zbMATHGoogle Scholar
  51. 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. 52.
    Knuth, D.E.: Verification of Link-Level Protocols. BIT 21, 31–36 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  53. 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)zbMATHCrossRefGoogle Scholar
  54. 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)CrossRefGoogle Scholar
  55. 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. 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)CrossRefGoogle Scholar
  57. 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. 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. 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)CrossRefGoogle Scholar
  60. 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)CrossRefGoogle Scholar
  61. 61.
    Postel, J.: Internet Protocol - DARPA Internet Program Protocol Specification. RFC 791, IETF (September 1981)Google Scholar
  62. 62.
    Postel, J.: Transmission Control Protocol. RFC 793 (1981)Google Scholar
  63. 63.
    Reisig, W.: Elements of Distributed Algorithms: Modelling and Analysis with Petri Nets. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  64. 64.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall International Series in Computer Science (1998)Google Scholar
  65. 65.
    Sabnani, K.: An Algorithmic Technique for Protocol Verification. IEEE Transactions on Communications 36(8), 924–931 (1988)zbMATHCrossRefGoogle Scholar
  66. 66.
    Stallings, W.: Data and Computer Communications, 6th edn. Prentice Hall, Englewood Cliffs (2000)Google Scholar
  67. 67.
    Standard ML of New Jersey, http://cm.bell-labs.com/cm/cs/what/smlnj/
  68. 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. 69.
    Stevens, W.R.: TCP/IP Illustrated, vol. 1. Addison-Wesley, Reading (1994)zbMATHGoogle Scholar
  70. 70.
    Sunshine, C.A.: Formal Techniques for Protocol Specification and Verification. IEEE Computer, 346-350 (September 1979)Google Scholar
  71. 71.
    Suzuki, I.: Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets. IEEE Transactions on Software Engineering 16(11), 1273–1281 (1990)CrossRefGoogle Scholar
  72. 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)CrossRefGoogle Scholar
  73. 73.
    Tanenbaum, A.: Computer Networks, 4th edn. Prentice Hall, Englewood Cliffs (2003)Google Scholar
  74. 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)CrossRefGoogle Scholar
  75. 75.
    Tomlinson, R.S.: Selecting sequence numbers. In: Proc. of SIGCOMM/SIGOPS Interprocess Commun. Workshop, pp. 11–23. ACM, New York (1975)CrossRefGoogle Scholar
  76. 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. 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. 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. 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. 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)CrossRefGoogle Scholar
  81. 81.
  82. 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. 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)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Jonathan Billington
    • 1
  • Guy Edward Gallasch
    • 1
  • Bing Han
    • 1
  1. 1.Computer Systems Engineering CentreUniversity of South AustraliaAustralia

Personalised recommendations