cpncourse

KO | EN

gitlite — search

#react #llm #go #docker #nodejs #macos #java #cli #kubernetes #vue #awesome-list #pytorch #ios #openai

(★ 29)

Coloured Petri Nets and CPN Tools Course

cpncourse Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# Course on Coloured Petri Nets and CPN Tools

- 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

## Reading and Preparation

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.

## Module I - Modelling and CPN Tools

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.

## Module II - Verification and Applications

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.

## Exercises and Assignments

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:

- https://github.com/lmkr/cpncourse/tree/master/models 
- https://github.com/lmkr/cpncourse/blob/master/assignment/assignment.md

cpncourse

cpncourse Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

cpncourse

cpncourse Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README