Coloured Petri Nets: A High Level Language for System Design and Analysis

  • K. Jensen

Abstract

This paper describes how Coloured Petri Nets (CP-nets) have been developed — from being a promising theoretical model to being a full-fledged language for the design, specification, simulation, validation and implementation of large software systems (and other systems in which human beings and/or computers communicate by means of some more or less formal rules).

First CP-nets are introduced by means of a small example and a formal definition of their structure and behaviour is presented. Then we describe how to extend CP-nets by a set of hierarchy constructs (allowing a hierarchical CP-net to consist of many different subnets, which are related to each other in a formal way). Next we describe how to analyse CP-nets, how to support them by various computer tools, and we also describe some typical applications. Finally, a number of future extensions are discussed (of the net model and the supporting software).

The non-hierarchical CP-nets in the present paper are analogous to the CP-nets defined in [35] and the High-level Petri Nets defined in [33]. In all three papers CP-nets (and HL-nets) have two different representations: The expression representation uses arc expressions and guards, while the function representation uses linear functions between multi-sets. Moreover, there are formal translations between the two representations (in both directions). In [33] and [35] we used the expression representation to describe systems, while we used the function representation for all the different kinds of analysis. It has, however, turned out that it only is necessary to turn to functions when we deal with invariant analysis, and this means that we now use the expression representation for all purposes — except for the calculation of invariants. This change is important for the practical use of CP-nets — because it means that the function representation and the translations (which are a bit mathematically complex) no longer are parts of the basic definition of CP-nets. Instead they are parts of the invariant method (which anyway demands considerable mathematical skills).

The development of CP-nets has been supported by several grants from the Danish National Science Research Council.

Keywords

Sugar Radar Coherence Dition Editing 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    K. Albert, K. Jensen and R.M. Shapiro: Design/CPN. A tool package supporting the use of Coloured Petri Nets. Petri Net Newsletter 32 (April 1989), 22–36.Google Scholar
  2. [2]
    J.L. Baer: Modelling architectural features with Petri nets. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986 Part II, Lecture Notes in Computer Science vol. 255, Springer-Verlag 1987, 258–277.Google Scholar
  3. [3]
    E. Best: Structure theory of Petri nets: the free choice hiatus. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986 Part I, Lecture Notes in Computer Science vol. 254, Springer-Verlag 1987, 168–205.Google Scholar
  4. [4]
    J. Billington, G. Wheeler and M. Wilbur-Ham: Protean: a high-level Petri net tool for the specification and verification of communication protocols. IEEE Transactions on. Software Engineering, Special Issue on Tools for Computer Communication Systems, SE-14(3), 1988, 301–316.Google Scholar
  5. [5]
    W. Brauer (ed.): Net theory and applications. Proceedings of the Advanced Course on General Net Theory of Processes and Systems, Hamburg 1979, Lecture Notes in Computer Science vol. 84, Springer-Verlag 1980, 213–223.Google Scholar
  6. [6]
    W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri nets: Central models and their properties. Advances in Petri Nets 1986 Part I, Lecture Notes in Computer Science vol. 254, Springer-Verlag 1987Google Scholar
  7. [7]
    W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri nets: Applications and relationships to other models of concurrency. Advances in Petri Nets 1986 Part II, Lecture Notes in Computer Science vol. 255, Springer-Verlag 1987Google Scholar
  8. [8]
    G. Chehaibar: Validation of phase-executed protocols modelled with coloured Petri nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 84–103.Google Scholar
  9. [9]
    G. Chiola, C. Dutheillet, G. Franceschinis and S. Haddad: On well-formed coloured nets and their symbolic reachability graph. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 387–411.Google Scholar
  10. [10]
    C. Choppy and C. Johnen: Petrireve: proving Petri net properties with rewriting systems. J.P. Jouannaud (ed.): Rewriting Techniques and Applications, Lecture Notes in Computer Science vol. 202, Springer-Verlag 1985, 271–286.Google Scholar
  11. [11]
    B. Cousin et. al.: Validation of a protocol managing a multi-token ring architecture. Proceedings of the 9th European Workshop on Applications and Theory of Petri Nets, Vol. II, Venice 1988.Google Scholar
  12. [12]
    J.M. Couvreur: The general computation of flows for coloured Petri nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 204–223.Google Scholar
  13. [13]
    F. De Cindio, G. Lanzarone and A. Torgano: A Petri net model of SDL. Proceedings of the 5th European Workshop on Applications and Theory of Petri Nets, Aarhus 1984, 272–289.Google Scholar
  14. [14]
    M. Diaz: Petri net based models in the specification and verification of protocols. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986 Part II, Lecture Notes in Computer Science vol. 255, Springer-Verlag 1987, 135–170.Google Scholar
  15. [15]
    R. Di Giovanni: Putting Petri nets into use: the Columbus programme. Proceedings Of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 123–138.Google Scholar
  16. [16]
    P. Estraillier and C. Girault: Petri nets specification of virtual ring protocols. In: A. Pagnoni and G. Rozenberg (eds.): Applications and Theory of Petri Nets, Informatik-Fachberichte vol. 66, Springer-Verlag 1983, 74–85.Google Scholar
  17. [17]
    F. Feldbrugge: Petri net tool overview 1989. In: G. Rozenberg (ed.): Advances in Petri Nets 1989. Lecture Notes in Computer Science vol. 424, Springer-Verlag 1990, 151–178.Google Scholar
  18. [18]
    A. Finkel: A minimal coverability graph for Petri nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 1–21.Google Scholar
  19. [19]
    G. Florin, C. Kaiser, S. Natkin: Petri net models of a distributed election protocol on undirectional ring. Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn 1989, 154–173.Google Scholar
  20. [20]
    H.J. Genrich and K. Lautenbach: System modelling with high-level Petri nets. Theoretical Computer Science 13 (1981), 109–136.CrossRefMATHMathSciNetGoogle Scholar
  21. [21]
    H.J. Genrich: Projections of C/E-systems. In: G. Rozenberg (ed.): Advances in Petri Nets 1985. Lecture Notes in Computer Science vol. 222, Springer-Verlag 1986, 224–232.Google Scholar
  22. [22]
    H.J. Genrich: Predicate/Transition nets. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986 Part I, Lecture Notes in Computer Science vol. 254, Springer-Verlag 1987, 207–247.Google Scholar
  23. [23]
    H.J. Genrich: Equivalence transformations of PrT-nets. In: G. Rozenberg (ed.): Advances in Petri Nets 1989, Lecture Notes in Computer Science, vol. 424, Springer-Verlag 1990, 179–208.Google Scholar
  24. [24]
    C. Girault, C. Chatelain and S. Haddad: Specification and properties of a cache coherence protocol model. In: G. Rozenberg (ed.): Advances in Petri Nets 1987, Lecture Notes in Computer Science, vol. 266, Springer-Verlag 1987, 1–20.Google Scholar
  25. [25]
    S. Haddad: A reduction theory for coloured nets. In: G. Rozenberg (ed.): Advances in Petri Nets 1989, Lecture Notes in Computer Science, vol. 424, Springer-Verlag 1990, 209–235.Google Scholar
  26. [26]
    R. Harper: Introduction to Standard ML. University of Edinburgh, Department of Computer Science, The King’s Buildings, Edinburgh EH9 3JZ, Technical Report ECS-LFCS-86–14, 1986.Google Scholar
  27. [27]
    R. Harper, D. MacQueen and R. Milner: Standard ML. University of Edinburgh, Department of Computer Science, The King’s Buildings, Edinburgh EH9 3JZ, Technical Report ECS-LFCS-86–2, 1986.Google Scholar
  28. [28]
    G. Hartung: Programming a closely coupled multiprocessor system with high level Petri nets. In: G. Rozenberg (ed.): Advances in Petri Nets 1988, Lecture Notes in Computer Science vol. 340, Springer-Verlag 1988, 154–174.Google Scholar
  29. [29]
    T. Hildebrand, H. Nieters, and N Trèves: The suitability of net-based Graspin tools for monetics applications. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 139–160.Google Scholar
  30. [30]
    P. Huber, A.M. Jensen, L.O. Jepsen and K. Jensen: Reachability trees for high-level Petri nets. Theoretical Computer Science 45 (1986), 261–292.CrossRefMATHMathSciNetGoogle Scholar
  31. [31]
    P. Huber, K. Jensen and R.M. Shapiro: Hierarchies in coloured Petri nets. In: G. Rozenberg (ed.): Advances in Petri Nets 1990, Lecture Notes in Computer Science, Springer-Verlag.Google Scholar
  32. [32]
    K. Jensen: Coloured Petri nets and the invariant method. Theoretical Computer Science 14 (1981), 317–336.CrossRefMathSciNetGoogle Scholar
  33. [33]
    K. Jensen: High-level Petri nets. In: A. Pagnoni and G. Rozenberg (eds.): Applications and Theory of Petri Nets, Informatik-Fachberichte vol. 66, Springer-Verlag 1983, 166–180.Google Scholar
  34. [34]
    K. Jensen and E.M. Schmidt: Pascal semantics by a combination of denotational semantics and high-level Petri nets. In: G. Rozenberg (ed.): Advances in Petri Nets 1985. Lecture Notes in Computer Science vol. 222, Springer-Verlag 1986, 297–329.Google Scholar
  35. [35]
    K. Jensen: Coloured Petri nets. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986 Part I, Lecture Notes in Computer Science vol. 254, Springer-Verlag 1987, 248–299.Google Scholar
  36. [36]
    K. Jensen et. al.: Design/CPN: A tool supporting coloured Petri nets. User’s manual, vol 1–2. Meta Software Corporation, 150 Cambridge Park Drive, Cambridge MA 02140, USA, 1988.Google Scholar
  37. [37]
    K. Jensen et. al.: Design/CPN extensions. Meta Software Corporation, 150 Cambridge Park Drive, Cambridge MA 02140, USA, 1990.Google Scholar
  38. [38]
    E. de Jong and M.R. van Steen: Vista: a specification language for parallel software design. Proceedings of the 3rd International Workshop on Software Engineering and its Applications, Toulouse, 1990.Google Scholar
  39. [39]
    A. Karsenty: Interactive graphical reporting facilities for Design/CPN. Master Thesis, University of Paris Sud, Computer Science Department, 1990.Google Scholar
  40. [40]
    R.M. Karp and R.E. Miller: Parallel program schemata. Journal of Computer and System Sciences, vol. 3, 1969, 147–195.CrossRefMATHMathSciNetGoogle Scholar
  41. [41]
    M. Lindqvist: Translation of the specification language SDL into predicate/transition nets. Licentiate’s Thesis, Helsinki University of Technology, Digital Systems Laboratory, 1987.Google Scholar
  42. [42]
    M. Lindqvist: Parameterized reachability trees for predicate/transition nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 22–42.Google Scholar
  43. [43]
    D.A. Marca and C.L. McGowan: SADT. McGraw-Hill, New York, 1988.Google Scholar
  44. [44]
    G. Memmi and J. Vautherin: Analysing nets by the invariant method. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986 Part I, Lecture Notes in Computer Science vol. 254, Springer-Verlag 1987, 300336.Google Scholar
  45. [45]
    Y. Narahari: On the invariants of coloured Petri nets. In: G. Rozenberg (ed.): Advances in Petri Nets 1985. Lecture Notes in Computer Science vol. 222, Springer-Verlag 1986, 330–345.Google Scholar
  46. [46]
    H. Oberquelle: Human-machine interaction and role/function/action-nets. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986 Part II, Lecture Notes in Computer Science vol. 255, Springer-Verlag 1987, 171–190.Google Scholar
  47. [47]
    Petri nets and performance models. Proceedings of the third international workshop, Kyoto Japan 1989, IEEE computer society press, order number 2001, ISBN 0–8186-20001–3.Google Scholar
  48. [48]
    C.A. Petri: Kommunikation mit automaten. Schriften des IIM Nr. 2, Institut für Instrumentelle Mathematik, Bonn, 1962. English translation: Technical Report RADC-TR-65–377, Griffiss Air Force Bas, New York, Vol. 1, Suppl. 1, 1966.Google Scholar
  49. [49]
    V.O. Pinci and R.M. Shapiro: Development and implementation of a strategy for electronic funds transfer by means of hierarchical coloured Petri nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 161–180.Google Scholar
  50. [50]
    C. Reade: Elements of functional programming. Addison Wesly, International Computer Science Series, ISBN 0–201–12915–9, 1989.Google Scholar
  51. [51]
    G. Rozenberg: Behaviour of elementary net systems. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986 Part I, Lecture Notes in Computer Science vol. 254, Springer-Verlag 1987, 60–94.Google Scholar
  52. [52]
    M. Rukoz and R. Sandoval.: Specification and correctness of distributed algorithms by coloured Petri nets. Proceedings of the 9th European Workshop on Applications and Theory of Petri Nets, Vol. II, Venice 1988.Google Scholar
  53. [53]
    Functional specification and description language SDL. In: CCITT Yellow Book, Vol. VI, recommendations Z.101 - Z.104, CCITT, Geneva, 1981.Google Scholar
  54. [54]
    R.M. Shapiro: Validation of a VLSI chip using hierarchical coloured Petri nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 224–243.Google Scholar
  55. [55]
    R.M. Shapiro, V.O. Pinci and R. Mameli: Modelling a NORAD command post using SADT and coloured Petri nets. Proceedings of the IDEF Users Group, Washington DC, May 1990.Google Scholar
  56. [56]
    M. Silva and R. Valette: Petri nets and flexible manufacturing. In: G. Rozenberg (ed.): Advances in Petri Nets 1989, Lecture Notes in Computer Science, vol. 424, Springer-Verlag 1990, 374–417.Google Scholar
  57. [57]
    P.S. Thiagarajan: Elementary net systems. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986 Part I, Lecture Notes in Computer Science vol. 254, Springer-Verlag 1987, 26–59.Google Scholar
  58. [58]
    R. Valk: Nets in computer organization. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986 Part II, Lecture Notes in Computer Science vol. 255, Springer-Verlag 1987, 218–233.Google Scholar
  59. [59]
    A. Valmari: Stubborn sets for reduced state space generation. Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn 1989, Vol II.Google Scholar
  60. [60]
    A. Valmari: Compositional state space generation. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, 43–62.Google Scholar
  61. [61]
    K. Voss: Nets in data bases. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986 Part II, Lecture Notes in Computer Science vol. 255, Springer-Verlag 1987, 97–134.Google Scholar
  62. [62]
    K. Voss: Nets in office automation. In: W. Brauer, W. Reisig and G. Rozenberg (eds.): Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986 Part II, Lecture Notes in Computer Science vol. 255, Springer-Verlag 1987, 234–257.Google Scholar
  63. [63]
    A. Wikström: Functional programming using Standard ML. Prentice Hall International Series in Computer Science, ISBN 0–13–331968–7, ISBN 0–13–331661–0 Pbk, 1987Google Scholar
  64. [64]
    E. Yourdon: Managing the system life cycle. Yourdon Press, 1982.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • K. Jensen

There are no affiliations available

Personalised recommendations