Skip to main content
Log in

Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems

  • Special Section CPN 04/05
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Coloured Petri Nets (CPNs) is a language for the modelling and validation of systems in which concurrency, communication, and synchronisation play a major role. Coloured Petri Nets is a discrete-event modelling language combining Petri nets with the functional programming language Standard ML. Petri nets provide the foundation of the graphical notation and the basic primitives for modelling concurrency, communication, and synchronisation. Standard ML provides the primitives for the definition of data types, describing data manipulation, and for creating compact and parameterisable models. A CPN model of a system is an executable model representing the states of the system and the events (transitions) that can cause the system to change state. The CPN language makes it possible to organise a model as a set of modules, and it includes a time concept for representing the time taken to execute events in the modelled system. CPN Tools is an industrial-strength computer tool for constructing and analysing CPN models. Using CPN Tools, it is possible to investigate the behaviour of the modelled system using simulation, to verify properties by means of state space methods and model checking, and to conduct simulation-based performance analysis. User interaction with CPN Tools is based on direct manipulation of the graphical representation of the CPN model using interaction techniques, such as tool palettes and marking menus. A license for CPN Tools can be obtained free of charge, also for commercial use.

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

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. Adamski, M.A., Karatkevich, A.,Wegrzyn, M. (eds). (2005). Design of Embedded Control Systems. Springer, Berlin

    Google Scholar 

  2. Andradóttir, S.: Simulation optimization. In: Banks [3], chap. 9

  3. Banks, J. (ed.): (1998). Handbook of Simulation. Wiley, New York

    Google Scholar 

  4. Billington, J.: ISO/IEC 15909-1:2004 Software and system engineering. High-level Petri nets, Part 1: Concepts, definitions and graphical notation, 2004

  5. Billington, J., Diaz, M., Rozenberg, G. (eds.): (1999). Application of Petri Nets to Communication Networks, vol. 1605. Springer, Berlin

    Google Scholar 

  6. 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. Advances in Petri Nets. In: Proceedings of 4th Advanced Course on Petri Nets, Lecture Notes in Computer Science, vol. 3018 pp. 210–290. Springer, Berlin (2004)

  7. BRITNeY Suite. http://www.wiki.daimi.au.dk/britney/

  8. Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured Petri Nets exploiting strongly connected components. In: Proceedings of International Workshop on Discrete Event Systems, pp. 169–177 (1996)

  9. Christensen, S., Kristensen, L.M., Mailund, T.: Condensed state spaces for timed Petri Nets. In: Proceedings of International Conference on Application and Theory of Petri Nets. Lecture Notes in Computer Science, vol. 2075 pp. 101–120. Springer, Berlin (2001)

  10. CPN Tools.: http://www.daimi.au.dk/CPNTools/

  11. Desrochers, A.A., Al-Jaar, R.Y.: Applications of Petri Nets in Manufacturing Systems: Modeling, Control, and Performance Analysis. IEEE, (1994)

  12. Examples of Industrial Use of CP-nets. http://www.daimi. au.dk/CPnets/intro/example_indu.html

  13. Gallasch, G.E., Kristensen, L.M.: COMMS/CPN: A Communication Infrastructure for External Communication with Design/CPN. In: Proceedings of Third Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB-554, pp. 75–91. Department of Computer Science, University of Aarhus, Denmark (2001)

  14. Gnuplot.: http://www.gnuplot.info

  15. ITU (CCITT).: Recommendation Z.120: MSC. Technical report, International Telecommunication Union, 1992

  16. Jensen K. (1992). Coloured Petri Nets. Basic concepts, analysis methods and practical use. Basic Concepts, vol. 1. Springer, Berlin

    Google Scholar 

  17. Jensen K. (1994). Coloured Petri Nets. Basic concepts, analysis methods and practical use. Analysis Methods, vol. 2. Springer, Berlin

    Google Scholar 

  18. Jensen, K. Condensed state spaces for symmetrical Coloured Petri Nets Formal Methods in System Design, vol. 9, (1996)

  19. Jensen K. (1997). Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Practical use, vol. 3. Springer, Berlin

    Google Scholar 

  20. Jensen, K., Kristensen, L.M.: Coloured Petri Nets. Modelling and Validation of Concurrent Systems. Springer Textbook (in preparation) Companion web site: www.daimi.au.dk/CPnets/ cpnbook.

  21. Kelton, W.D., Sadowski, R.P., Sadowski, D.A.: Simulation with Arena, 2nd edn. McGraw-Hill, (2002)

  22. Kleijnen, J.P.C.: Experimental design for sensitivity analysis, optimization, and validation of simulation models. In: Banks [3]

  23. Kristensen L.M., Christensen S. and Jensen K. (1998). The Practitioner’s Guide to Coloured Petri Nets. Int. J. Softw. Tools Technol. Transf. 2(2): 98–132

    Article  MATH  Google Scholar 

  24. Kristensen, L.M., Jørgensen, J.B., Jensen, K.: Application of Coloured Petri Nets in System Development. In: Lectures on Concurrency and Petri Nets. Advances in Petri Nets. Proceedings of 4th Advanced Course on Petri Nets. Lecture Notes in Computer Science, vol. 3098, pp. 626–685. Springer, Berlin (2004)

  25. Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Proceedings of Formal Methods Europe, Lecture Notes in Computer Science, vol. 2391, pp. 549–567. Springer, Berlin (2002)

  26. Kristensen, L.M., Valmari, A.: Finding Stubborn Sets of Coloured Petri Nets Without Unfolding. In: Proceedings of International Conference on Application and Theory of Petri Nets. Lecture Notes in Computer Science, vol. 1420, pp. 104–123. Springer, Berlin (1998)

  27. Law, A.M., Kelton, W.D.: Simulation Modeling and Analysis, 3rd edn. McGraw-Hill, (2000)

  28. Mortensen, K.H.: Efficient data-structures and algorithms for a Coloured Petri Nets Simulator. In: Proceedings of Third Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, 2001

  29. Object Management Group. Unified Modeling Language: Superstructure, version 2.0, formal/05-07-04, 2005

  30. Proceedings of International Conference on Application and Theory of Petri Nets and Other Models of Concurrency. Springer, Berlin 1980–present

  31. Proceedings of Workshop on Modelling of Objects, Components, and Agents, 2001–present

  32. Proceedings of Workshop on Practical Use of Coloured Petri Nets and the CPN Tools, 1998–present. http://www.daimi. au.dk/CPnets/

  33. Reisig W. (1985). Petri Nets. EATCS Monographs on Theoretical Computer Science, vol. 4. Springer, Berlin

    Google Scholar 

  34. Reisig W. (1998). Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets. Springer, Berlin

    MATH  Google Scholar 

  35. SceneBeans. http://www.dse.doc.ic.ac.uk/Software/SceneBeans/

  36. Standard ML of New Jersey. http://www.smlnj.org

  37. Ullman J.D. (1998). Elements of ML Programming. Prentice-Hall, Englewood Cliffs

    Google Scholar 

  38. Valmari, A.: The state explosion problem. In: Lectures on Petri Nets I: Basic Models. Lecture Notes in Computer Science, vol. 1491 pp. 429–528. Springer, Berlin (1998)

  39. Aalst W. and Hee K. (2002). Workflow Management: Models, Methods and Systems. MIT Press, Cambridge, MA

    Google Scholar 

  40. Westergaard, M., Lassen, K.B.: The BRITNeY Suite Animation Tool. In: Proceedings of 27th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency. Lecture Notes in Computer Science, vol. 4024 pp. 431–440. Springer, Berlin (2006)

  41. Yakovlev A., Gomes L. and Lavagno L. (2000). Hardware Design and Petri Nets. Springer, Berlin

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Lisa Wells.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Jensen, K., Kristensen, L.M. & Wells, L. Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. Int J Softw Tools Technol Transfer 9, 213–254 (2007). https://doi.org/10.1007/s10009-007-0038-x

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-007-0038-x

Keywords

Navigation