Jensen / Kristensen Coloured Petri Nets

Modelling and Validation of Concurrent Systems
1. Auflage 2009
ISBN: 978-3-642-00284-7
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 384 Seiten

Coloured Petri Nets (CPN) is a graphical language for modelling and validating concurrent and distributed systems, and other systems in which concurrency plays a major role. The development of such systems is particularly challenging because of inherent intricacies like possible nondeterminism and the immense number of possible execution sequences. In this textbook Jensen and Kristensen introduce the constructs of the CPN modelling language and present the related analysis methods in detail. They also provide a comprehensive road map for the practical use of CPN by showcasing selected industrial case studies that illustrate the practical use of CPN modelling and validation for design, specification, simulation, verification and implementation in various application domains. Their presentation primarily aims at readers interested in the practical use of CPN. Thus all concepts and constructs are first informally introduced through examples and then followed by formal definitions (which may be skipped). The book is ideally suitable for a one-semester course at an advanced undergraduate or graduate level, and through its strong application examples can also serve for self-study. An accompanying website offers additional material such as slides, exercises and project proposals. Book website: http://www.cs.au.dk/CPnets/cpnbook/

Autoren/Hrsg.

Jensen, Kurt

Kristensen, Lars M.

Inhaltsverzeichnis

1;Preface;5
2;Contents;8
3;Chapter 1 Introduction to Modelling and Validation;11
3.1;Modelling and System Development;11
3.2;Coloured Petri Nets;13
3.3;Abstraction and Visualisation;15
3.4;Formal Modelling and Verification;16
3.5;CPN Tools;18
3.6;Industrial Applications;21
4;Chapter 2 Non-hierarchical Coloured Petri Nets;23
4.1;A Simple Example Protocol;23
4.2;Net Structure and Inscriptions;24
4.3;Enabling and Occurrence of Transitions;27
4.4;Second Model of the Protocol;34
4.5;Concurrency and Conflict;39
4.6;Guards;44
4.7;Interactive and Automatic Simulation;45
5;Chapter 3 CPN ML Programming;52
5.1;Functional Programming;52
5.2;Colour Sets;54
5.3;Expressions and Types;65
5.4;Functions;69
5.5;Recursion and Lists;74
5.6;Patterns;79
5.7;Computation of Enabled Binding Elements;82
6;Chapter 4 Formal Definition of Non-hierarchical Coloured Petri Nets;87
6.1;Multisets;88
6.2;Net Structure and Inscriptions;91
6.3;Enabling and Occurrence of Steps;95
7;Chapter 5 Hierarchical Coloured Petri Nets;103
7.1;Modules and Interfaces;103
7.2;Module Instances and Hierarchy;108
7.3;Instance Folding and Module Parameterisation;113
7.4;Model Parameterisation;120
7.5;Fusion Sets;124
7.6;Unfolding Hierarchical CPN Models;132
8;Chapter 6 Formal Definition of Hierarchical Coloured Petri Nets;134
8.1;Modules;134
8.2;Module Composition;138
8.3;Instances and Compound Places;143
8.4;Enabling and Occurrence of Steps;148
9;Chapter 7 State Spaces and Behavioural Properties;157
9.1;Protocol for State Space Analysis;158
9.2;State Spaces;159
9.3;Strongly-Connected-Component Graphs;166
9.4;Behavioural Properties;169
9.5;Error Diagnostics and Counterexamples;186
9.6;Limitations of State Spaces;191
10;Chapter 8 Advanced State Space Methods;194
10.1;State Space Reduction Methods;194
10.2;Sweep-Line Method;196
10.3;Symmetry Method;199
10.4;Equivalence Method;203
11;Chapter 9 Formal Definition of State Spaces and Behavioural Properties;207
11.1;Directed Graphs;207
11.2;State Spaces;213
11.3;Reachability Properties;215
11.4;Basic Boundedness Properties;217
11.5;Generalised Boundedness Properties;220
11.6;Home Properties;223
11.7;Liveness Properties;226
11.8;Fairness Properties;231
12;Chapter 10 Timed Coloured Petri Nets;234
12.1;First Timed Model of the Protocol;235
12.2;Second Timed Model of the Protocol;246
12.3;State Space Analysis of Timed Models;250
12.4;Time Equivalence Method;255
13;Chapter 11 Formal Definition of Timed Coloured Petri Nets;259
13.1;Timed multisets;259
13.2;Net Structure and Inscriptions;266
13.3;Enabling and Occurrence of Steps;267
14;Chapter 12 Simulation-based Performance Analysis;274
14.1;Timed Protocol for Performance Analysis;275
14.2;Data Collection from the Occurring Binding Elements;279
14.3;Data Collection from the Markings Reached;282
14.4;Collecting Data from the Final Marking;287
14.5;Simulation Output;288
14.6;Conducting Simulation Experiments;292
14.7;Model Parameters and Configurations;296
15;Chapter 13 Behavioural Visualisation;303
15.1;Message Sequence Charts;304
15.2;System-Specific Interaction Graphics;308
16;Chapter 14 Examples of Industrial Applications;313
16.1;Protocol Design at Ericsson Telebit;314
16.2;Requirements Engineering at Systematic;329
16.3;Embedded-System Design at Bang and Olufsen;338
16.4;Scheduling Tool for Australian Defence Forces;350
17;Chapter 15 Teaching Coloured Petri Nets;362
17.1;Course Context and Aims;362
17.2;Intended Learning Outcomes;363
17.3;Teaching and Assessment Methods;366
17.4;Example of a Student Project from the Course;369
17.5;Experiences from Teaching the CPN Course;371
18;References;374
19;Index;379