- CPN Tools can downloaded from here: www.cpntools.org
- The homepage for the CPN book can be found here: https://github.com/lmkr/cpnbook/blob/master/README.md
The CPN modules are based on the book chapters and papers listed below:
- Chapters 1 and 2 of the book "Coloured Petri Nets": https://github.com/lmkr/cpnbook/blob/master/README.md
- The CPN papers avaiable via: https://github.com/lmkr/cpncourse/tree/master/papers
In the two modules on Coloured Petri Nets, we will use the CPN Tools available via. http://www.cpntools.org It is recommended to download and install the tool on your PC before attending the Petri Net Course. If you have any technical problems with the installation please see http://cpntools.org/support or contact the lecturer.
The first module focusses on the constructs and definition of the Coloured Petri Nets (CPNs) modelling language. CPNs belong to the class of high-level Petri nets and combines Petri Nets with the functional programming language Standard ML (SML). Petri nets provides the primitives for modelling concurrency, communication, and synchronisation while SML provides the primitives for modelling data manipulation and for creating compact and parameterised models. CPNs and the supporting computer tool CPN Tools have been widely used in practice for modelling and validating a wide range of concurrent and distributed systems. Having completed this module the participants should be able to:
- explain and use the basic constructs of the CPN modelling language
- explain the syntax and semantics of CPNs
- structure CPN models into a hierarchically related set of modules
- apply CPN Tools for construction and simulation of CPN models
The module includes hands-on experiments with CPN Tools.
Explicit state space exploration is one of the main approaches to computer-aided verification of concurrent systems, and it is one of the main analysis methods for Coloured Petri Nets (CPNs). This module provides an introduction to state space methods in the context of CPNs, and explains how standard behavioural properties of CPNs can be verified fully automatically using state spaces and the support for state space exploration provided by CPN Tools. The module also introduces the basics of temporal logic and associated model checking algorithms for verifying more general behavioral properties of concurrent systems. Examples demonstrating the practical use of CPN modelling and verification on industrial-sized systems will be presented. Having completed this module the participants should be able to:
- define standard behavioural properties of CPNs and express behavioral properties in temporal logic
- explain the basic concepts of state spaces and how they are computed
- explain how behavioural properties can be automatically checked from state spaces
- apply state spaces and model checking techniques for verification of CPN models
The module includes hands-on experiments with CPN Tools.
The CPN models used during the lectures and a description of the assignment to complete for the CPN part (in case you want ECTS credits) are available via: