Very Brief Introduction to Coloured Petri NetsColoured Petri Nets (CP-nets or CPNs) is a modelling language developed for systems in which communication, synchronisation and resource sharing play an important role. CP-nets combine the strengths of ordinary Petri nets with the strengths of a high-level programming language. Petri nets provide the primitives for process interaction, while the programming language provides the primitives for the definition of data types and the manipulations of data values.CP-nets has an intuitive, graphical representation which is appealing to human beings. A CPN model consists of a set of modules (pages) which each contains a network of places, transitions and arcs. The modules interact with each other through a set of well-defined interfaces, in a similar way as known from many modern programming languages. The graphical representation makes it easy to see the basic structure of a complex CPN model, i.e., understand how the individual processes interact with each other. CP-nets also has a formal, mathematical representation with a well-defined syntax and semantics. This representation is the foundation for the definition of the different behavioural properties and the analysis methods. Without the mathematical representation it would have been totally impossible to develop a sound and powerful CPN language. However, for the practical use of CP-nets and their tools, it suffices to have an intuitive understanding of the syntax and semantics. This is analogous to programming languages which are successfully applied by users who are not familiar with the formal, mathematical definitions of the languages. CPN models can be made with or without explicit reference to time. Untimed CPN models are usually used to validate the functional/logical correctness of a system, while timed CPN models are used to evaluate the performance of the system. There are many other languages which can be used to investigate the functional/logical correctness of a system or the performance of it. However, it is rather seldom to find modelling languages that are well-suited for both kinds of analysis. CP-nets can be simulated interactively or automatically. In an interactive simulation the user is in control. It is possible to see the effects of the individual steps directly on the graphical representation of the CP-net. This means that the user can investigate the different states and choose between the enabled transitions. An interactive simulation is similar to single-step debugging. It provides a way to "walk through" a CPN model, investigating different scenarios and checking whether the model works as expected. This is in contrast to many off-the-shelf simulation packages which often act as black boxes, where the user can define inputs and inspect the results, but otherwise have very little possibility to understand and validate the models on which the simulations build. It is our experience that the insight and detailed knowledge of a system, which the users gain during the development and validation of a simulation model, is often as important as the results that the users get from the actual simulation runs. Automatic simulations are similar to program executions. Now the purpose is to be able to execute the CPN models as fast and efficient as possible, without detailed human interaction and inspection. However, the user still needs to interpret the simulation results. For this purpose it is often suitable to use animated, graphical representations providing an abstract, application-specific view of the current state and activities in the system. CP-nets also offers more formal verification methods, known as state space analysis and invariant analysis. In this way it is possible to prove, in the mathematical sense of the word, that a system has a certain set of behavioural properties. However, industrial systems are often so complex that it is impossible or at least very expensive to make a full proof of system correctness. Hence, the formal verification methods should be seen as a complement to the more informal validation by means of simulation. The use of formal verification is often restricted to the most important subsystems or the most important aspects of a complex system. CP-nets and their tools have been used in numerous practical projects within a large variety of different application areas. The CPN group at the University of Aarhus, Denmark, has developed two sets of computer tools, supporting the use of CP-nets:
| |
Last modified: Sun Dec 28 14:25:47 2003 -- CP-nets Webmaster |