Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical UseThis book presents a coherent description of the theoretical and practical aspects of Coloured Petri Nets (CP-nets or CPN). It shows how CP-nets have been de veloped - from being a promising theoretical model to being a full-fledged lan guage for the design, specification, simulation, validation and implementation of large software systems (and other systems in which human beings and/or com puters communicate by means of some more or less formal rules). The book contains the formal definition of CP-nets and the mathematical theory behind their analysis methods. However, it has been the intention to write the book in such a way that it also becomes attractive to readers who are more interested in applications than the underlying mathematics. This means that a large part of the book is written in a style which is closer to an engineering textbook (or a users' manual) than it is to a typical textbook in theoretical computer science. The book consists of three separate volumes. The first volume defines the net model (i. e. , hierarchical CP-nets) and the basic concepts (e. g. , the different behavioural properties such as deadlocks, fair ness and home markings). It gives a detailed presentation of many small exam ples and a brief overview of some industrial applications. It introduces the for mal analysis methods. Finally, it contains a description of a set of CPN tools which support the practical use of CP-nets. |
Contents
Informal Introduction to Coloured Petri Nets | 1 |
11 Introduction to PlaceTransition Nets | 2 |
12 Introduction to Coloured Petri Nets | 8 |
Distributed Data Base | 21 |
14 Net Inscriptions in CPN ML | 26 |
15 Construction of CPN Models | 32 |
16 Drawing of CPN Diagrams | 41 |
17 Some Important Advantages of CPnets | 50 |
43 Home Properties | 131 |
44 Liveness Properties | 132 |
45 Fairness Properties | 135 |
Bibliographical Remarks | 138 |
Formal Analysis of Coloured Petri Nets | 141 |
51 Occurrence Graphs | 142 |
52 Place and Transition Invariants | 147 |
53 Reduction Rules | 150 |
Bibliographical Remarks | 52 |
Exercises | 55 |
Formal Definition of Coloured Petri Nets | 65 |
21 Multisets | 66 |
22 Structure of NonHierarchical CPnets | 69 |
23 Behaviour of NonHierarchical CPnets | 73 |
24 Equivalent PlaceTransition Nets | 78 |
Bibliographical Remarks | 85 |
Hierarchical Coloured Petri Nets | 89 |
31 Introduction to Hierarchical CPnets | 90 |
Telephones | 99 |
33 Structure of Hierarchical CPnets | 106 |
34 Behaviour of Hierarchical CPnets | 113 |
35 Equivalent NonHierarchical CPnets | 115 |
Bibliographical Remarks | 119 |
Dynamic and Static Properties of Coloured Petri Nets | 123 |
41 Static Properties | 124 |
42 Boundedness Properties | 127 |
54 Performance Analysis | 152 |
Exercises | 153 |
Computer Tools for Coloured Petri Nets | 155 |
61 Editing of CPnets | 156 |
62 Simulation of CPnets | 176 |
63 Computer Tools for Formal Analysis | 194 |
Bibliographical Remarks | 202 |
Industrial Applications of Coloured Petri Nets | 205 |
71 Communication Protocol | 206 |
72 Hardware Chip | 209 |
73 Radar Surveillance | 213 |
74 Electronic Funds Transfer | 217 |
75 General Observations About CPN Applications | 218 |
Bibliographical Remarks | 219 |
References | 221 |
231 | |
Other editions - View all
Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use ... Kurt Jensen Limited preview - 2013 |
Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use ... Kurt Jensen No preview available - 1997 |
Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use ... Kurt Jensen No preview available - 2010 |
Common terms and phrases
Advances in Petri allows the user Analogously arc expressions behaviour binding elements Chap code segments colour set Coloured Petri Nets command complex Computer Science Vol constructed contains corresponding CPN diagram CPN editor CPN ML CPN model CPN simulator CPN tools declarations defined definition denote described dialogue box e-tokens empty equivalence relation evaluates example Exercise function fusion set graphical guard hierarchical CP-net high-level nets IDEF Inactive initial marking initialization expressions input inscriptions integer invariants Lecture Notes M₁ means Message multi-set nodes non-hierarchical CP-net Notes in Computer objects occurrence graph occurrence sequences page instances place instance group places and transitions port assignment possible prime page programming languages properties PT-net PT-net transitions q-processes reachable marking regions represent resource allocation system ring network Rozenberg SADT Sect sender specified Springer-Verlag Standard ML step subnet subpage substitution transitions supernode tion token colours transition instance variables