Advertisement

Application of Coloured Petri Nets in System Development

  • Lars Michael Kristensen
  • Jens Bæk Jørgensen
  • Kurt Jensen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3098)

Abstract

Coloured Petri Nets (CP-nets or CPNs) and their supporting computer tools have been used in a wide range of application areas such as communication protocols, software designs, and embedded systems. The practical application of CP-nets has also covered many phases of system development ranging from requirements to design, validation, and implementation. This paper presents four case studies where CP-nets and their supporting computer tools have been used in system development projects with industrial partners. The case studies have been selected such that they illustrate different application areas of CP-nets in various phases of system development.

Keywords

State Space Global Clock State Space Method Substitution Transition State Space Analysis 
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.
    Aarhus Amt Electronic Patient Record, http://www.epj.aaa.dk
  2. 2.
    Amyot, D., Buhr, R.J.A., Gray, T., Logrippo, L.: Use Case Maps for the Capture and Validation of Distributed Systems Requirements. In: Proc. of 4th IEEE International Symposium on Requirements Engineering, pp. 44–53. IEEE Computer Society, Los Alamitos (1999)Google Scholar
  3. 3.
    Antón, A.I., Carter, R.A., Dagnino, A., Dempster, J.H., Siege, D.F.: Deriving Goals from a Use-Case Based Requirements Specification. Requirements Engineering Journal 6, 63–73 (2001)zbMATHCrossRefGoogle Scholar
  4. 4.
    Australian Defence Science and Technology Organisation, http://www.dsto.defence.gov.au
  5. 5.
  6. 6.
    Bardram, J.E., Bossen, C.: Moving to get aHead: Local Mobility and Collaborative Work. In: Proc. of 8th European Conference on Computer-supported Cooperative Work, pp. 355–374. Kluwer Academic Publishers, Dordrecht (2003)Google Scholar
  7. 7.
    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 (2004) (to appear)Google Scholar
  8. 8.
    Capellmann, C., Christensen, S., Herzog, U.: Visualising the Behaviour of Intelligent Networks. In: Margaria, T., Steffen, B., Rückert, R., Posegga, J. (eds.) AIN 1997, ICALP-WS 1997, VISUAL-WS 1998, ACoS 1998, and ETAPS-WS 1998. LNCS, vol. 1385, pp. 174–189. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    ITU (CCITT). Recommendation Z.120: MSC. Technical report, International Telecommunication Union (1992)Google Scholar
  10. 10.
    Centre for pervasive computing, http://www.pervasive.dk
  11. 11.
    Cheng, A., Christensen, S., Mortensen, K.H.: Model Checking Coloured Petri Nets Exploiting Strongly Connected Components. In: Proc. of the International Workshop on Discrete Event Systems, WODES 1996. Institution of Electrical Engineers, Computing and Control Division, Edinburgh, UK (1996)Google Scholar
  12. 12.
    Christensen, H.B., Bardram, J.E.: Supporting Human Activities – Exploring Activity-Centered Computing. In: Borriello, G., Holmquist, L.E. (eds.) UbiComp 2002. LNCS, vol. 2498, p. 107. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. 13.
    Christensen, S.: Message Sequence Charts. User’s Manual (January 1997)Google Scholar
  14. 14.
    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
  15. 15.
    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
  16. 16.
    Christensen, S., Kristensen, L.M., Mailund, T.: Condensed State Spaces for Timed Petri Nets. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 101–120. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  17. 17.
    Clarke, E., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry Reductions in Model Checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 147–159. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  18. 18.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  19. 19.
    Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting Symmetries in Temporal Logic Model Checking. Formal Methods in System Design 9(1/2), 77–104 (1996)CrossRefGoogle Scholar
  20. 20.
    Cockburn, A.: Writing Effective Use Cases. Addison-Wesley, Reading (2000)Google Scholar
  21. 21.
    Computer Systems Engineering Centre at University of South Australia, http://www.unisa.edu.au/eie/csec/
  22. 22.
  23. 23.
    The CPN Group at University of Aarhus, www.daimi.au.dk/CPnets
  24. 24.
    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
  25. 25.
  26. 26.
    Dulac, N., Viguier, T., Leveson, N., Storey, M.-A.: On the Use of Visualization in Formal Requirements Specification. In: Proc. of 7th IEEE International Symposium on Requirement Engineering, pp. 71–80. IEEE Computer Society, Los Alamitos (2002)Google Scholar
  27. 27.
    Jensen, K. (ed.): International Journal on Software Tools for Technology Transfer, vol. 2(2) (1998) (special section on Coloured Petri nets)Google Scholar
  28. 28.
    Jensen, K. (ed.): International Journal on Software Tools for Technology Transfer, vol. 3(4) (2001) (special section on Coloured Petri nets)Google Scholar
  29. 29.
    Elgaard, L.: The Symmetry Method for Coloured Petri Nets. PhD thesis, Department of Computer Science, University of Aarhus (July 2002)Google Scholar
  30. 30.
    Elkoutbi, M., Keller, R.K.: User Interface Prototyping Based on UML Scenarios and High-Level Petri Nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, p. 166. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  31. 31.
    Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative Temporal Reasoning. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 136–145. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  32. 32.
    Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. Formal Methods in System Design 9(1/2), 105–131 (1996)CrossRefGoogle Scholar
  33. 33.
    Ericsson Telebit A/S, http://www.ericssontelebit.dk
  34. 34.
    Esparza, J.: Model Checking using Net Unfoldings. Science of Computer Programming 23, 151–195 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  35. 35.
    Internet Engineering Task Force. Mobile ad-hoc networks, http://www.ietf.org/html.charters/manet-charter.html
  36. 36.
    Gallasch, G., Kristensen, L.M.: Comms/CPN: A Communication Infrastructure for External Communication with Design/CPN. In: Proc. of the 3rd Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Department of Computer Science, University of Aarhus, pp. 79–93 (2001) DAIMI PB-554Google Scholar
  37. 37.
    Gallasch, G.E., Kristensen, L.M., Mailund, T.: Sweep-Line State Space Exploration for Coloured Petri Nets. In: Proc. of 4th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Department of Computer Science, University of Aarhus, pp. 101–120 (2002) DAIMI PB-560Google Scholar
  38. 38.
    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
  39. 39.
    Holzmann, G.J.: Tracing Protocols. Bell System Technical Journal 64, 2413–2434 (1985)Google Scholar
  40. 40.
    G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International edn (1991)Google Scholar
  41. 41.
    Holzmann, G.J.: An Analysis of Bitstate Hashing. Formal Methods in System Design 13(3), 287–305 (1998)CrossRefMathSciNetGoogle Scholar
  42. 42.
    Huitema, C.: IPv6: The New Internet Protocol. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  43. 43.
    Ip, C.N., Dill, D.L.: Better Verification Through Symmetry. Formal Methods in System Design 9(1/2), 41–75 (1996)Google Scholar
  44. 44.
    Jackson, M.: System Development. Prentice-Hall, Englewood Cliffs (1983)zbMATHGoogle Scholar
  45. 45.
    Jacobson, M., Christerson, P.: Object-Oriented Software Engineering: A Use Case Driven Approach. Addison-Wesley, Reading (1992)zbMATHGoogle Scholar
  46. 46.
    Jard, C., Jeron, T.: Bounded-memory Algorithms for Verification On-the-fly. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 192–202. Springer, Heidelberg (1991)Google Scholar
  47. 47.
    Jensen, K.: Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use. Basic Concepts, vol. 1. Springer, Heidelberg (1992)zbMATHGoogle Scholar
  48. 48.
    Jensen, K.: Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use. Analysis Methods, vol. 2. Springer, Heidelberg (1995)zbMATHGoogle Scholar
  49. 49.
    Jensen, K.: Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design 9(1/2), 7–40 (1996)CrossRefGoogle 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.
    Jensen, K. (ed.): Proceedings Workshop and Tutorial on Practical Use of Coloured Petri Nets and CPN Tools (1998-2002), Available via http://www.daimi.au.dk/CPnets
  52. 52.
    Jørgensen, J.B.: Coloured Petri Nets in Development of a Pervasive Health Care System. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 256–275. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  53. 53.
    Jørgensen, J.B., Bossen, C.: Requirements Engineering for a Pervasive Health Care System. In: Proc. of 11th IEEE International Requirements Engineering Conference, pp. 55–64. IEEE Computer Sociery, Los Alamitos (2003)Google Scholar
  54. 54.
    Jørgensen, J.B., Bossen, C.: Executable Use Cases: Requirements for a Pervasive Health Care System. IEEE Software (March/April 2004) (to appear)Google Scholar
  55. 55.
    Jørgensen, J.B., Christensen, S.: Executable Design Models for a Pervasive Healthcare Middleware System. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 140–149. Springer, Heidelberg (2002)Google Scholar
  56. 56.
    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)CrossRefGoogle Scholar
  57. 57.
    Kristensen, L.M.: Ad-hoc Networking and IPv6: Modelling and Validation, http://www.pervasive.dk/projects/IPv6/IPv6_summary
  58. 58.
    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
  59. 59.
    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)CrossRefGoogle Scholar
  60. 60.
    Kristensen, L.M., Mailund, T.: A Compositional Sweep-Line State Space Exploration Method. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 327–343. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  61. 61.
    Kruchten, P.: The Rational Unified Process: An Introduction. Addison-Wesley, Reading (1999)Google Scholar
  62. 62.
    Lindstrøm, B.: Web-Based Interfaces for Simulation of Coloured Petri Net Models. International Journal on Software Tools for Technology Transfer 3(4), 405–416 (2001)Google Scholar
  63. 63.
    Lorentsen, L., Kristensen, L.M.: Exploiting Stabilizers and Parallelism in State Space Generation with the Symmetry Method. In: Proceedings of International Conference on Application of Concurrency in System Design, pp. 211–220. IEEE Computer Society, Los Alamitos (2001)CrossRefGoogle Scholar
  64. 64.
    Lorentsen, L., Tuovinen, A.-P., Xu, J.: Modelling Features and Feature Interactions of Nokia Mobile Phones Using Coloured Petri Nets. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, p. 294. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  65. 65.
    McMillan, K.L.: A Technique of State Space Search Based on Unfolding. Formal Methods in System Design 6(1), 45–65 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  66. 66.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  67. 67.
    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)CrossRefGoogle Scholar
  68. 68.
    Neill, C.J., Laplante, P.A.: Requirements Engineering: The State of the Practice. IEEE Software 20(6), 61–69 (2003)CrossRefGoogle Scholar
  69. 69.
    OMG Unified Modeling Language Specification, Version 1.4. Object Management Group (OMG); UML Revision Taskforce (2001)Google Scholar
  70. 70.
    Peled, D.: All from One, One for All: On Model Checking Using Representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)Google Scholar
  71. 71.
    Perkins, C.E.: Ad Hoc Networking. Addison-Wesley, Reading (2001)Google Scholar
  72. 72.
    Pervasive Healthcare, http://www.healthcare.pervasive.dk
  73. 73.
    Lawrence Pfleeger, S.: Software Engineering: Theory and Practice, 2nd edn. Prentice-Hall, Englewood Cliffs (2001)Google Scholar
  74. 74.
    Radio Frequency Identification, http://www.rfid.org
  75. 75.
    Rasmussen, J.L., Singh, M.: Mimic/CPN. A Graphical Simulation Utility for Design/CPN, User’s Manual, http://www.daimi.au.dk/designCPN
  76. 76.
    Rasmussen, J.L., Singh, M.: Designing a Security System by Means of Coloured Petri Nets. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 400–419. Springer, Heidelberg (1996)Google Scholar
  77. 77.
    Reisig, W.: Petri Nets. EACTS Monographs in Theoretical Computer Science, vol. 4. Springer, Heidelberg (1985)zbMATHGoogle Scholar
  78. 78.
    Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading (1999)Google Scholar
  79. 79.
  80. 80.
    Satyanarayanan, M.: Challenges in Implementing a Context-Aware System. In: Pervasive Computing, vol. 1(3). IEEE, Los Alamitos (2002)Google Scholar
  81. 81.
    Satyanarayanan, M. (ed.): Pervasive Computing, vol. 1(1). IEEE, Los Alamitos (2002)Google Scholar
  82. 82.
    Simons, A.J.H., Graham, I.: 30 Things That Go Wrong in Object Modelling with UML 1.3. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. Kluwer Academic Publishers, Dordrecht (1999)Google Scholar
  83. 83.
    Stallings, W.: Data & Computer Communications, 6th edn. Prentice Hall, Englewood Cliffs (2000)Google Scholar
  84. 84.
    Systematic Software Engineering A/S, http://www.systematic.dk
  85. 85.
  86. 86.
    Ullman, J.D.: Elements of ML Programming. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  87. 87.
    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 (1990)CrossRefGoogle Scholar
  88. 88.
    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
  89. 89.
    van Lamsweerde, A.: Requirements Engineering in the Year 2000: A Research Perspective. In: Proc. of the 22nd International Conference on Software Engineering. ACM Press, New York (2000)Google Scholar
  90. 90.
    Weiser, M.: The Computer for the 21st Century. Scientific American 265(3). Scientific American, Inc., Singapore (1991)Google Scholar
  91. 91.
    Wells, L.: Performance Analysis Using Coloured Petri Nets. In: Proc. of the Tenth IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. IEEE Computer Society, Los Alamitos (2002)Google Scholar
  92. 92.
    Wells, L., Christensen, S., Kristensen, L.M., Mortensen, K.: Simulation Based Performance Analysis of Web Servers. In: Proc. of the 9th International Workshop on Petri Nets and Performance Models, pp. 59–68. IEEE Computer Society, Los Alamitos (2001)CrossRefGoogle Scholar
  93. 93.
    Wolper, P., Godefroid, P.: Partial Order Methods for Temporal Verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 233–246. Springer, Heidelberg (1993)Google Scholar
  94. 94.
    Zhang, L., Kristensen, L.M., Janczura, C., Gallasch, G., Billington, J.: A Coloured Petri Net based Tool for Course of Action Development and Analysis. In: Proc. of Workshop on Formal Methods Applied to Defence Systems. Conferences in Research and Practice in Information Technology, vol. 12, pp. 125–134. Australian Computer Society (2001)Google Scholar
  95. 95.
    Zimmerman, M.K., Lundqvist, K., Leveson, N.: Investigating the Readability of State-Based Formal Requirements Specification Languages. In: Proc. of 24th International Conference on Software Engineering, pp. 33–43. ACM Press, New York (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Lars Michael Kristensen
    • 1
  • Jens Bæk Jørgensen
    • 1
  • Kurt Jensen
    • 1
  1. 1.Department of Computer ScienceUniversity of AarhusAarhus NDenmark

Personalised recommendations