Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems

Kurt Jensen, Lars Michael Kristensen, Lisa Wells

Abstract: Coloured Petri Nets (CPNs) is a language for the modelling and validation of systems in which concurrency, communication, and synchronisation play a major role. Coloured Petri Nets is a discrete-event modelling language combining Petri nets with the functional programming language Standard ML. Petri nets provide the foundation of the graphical notation and the basic primitives for modelling concurrency, communication, and synchronisation. Standard ML provides the primitives for the definition of data types, describing data manipulation, and for creating compact and parameterisable models. A CPN model of a system is an executable model representing the states of the system and the events (transitions) that can cause the system to change state. The CPN language makes it possible to organise a model as a set of modules, and it includes a time concept for representing the time taken to execute events in the modelled system.

CPN Tools is an industrial-strength computer tool for constructing and analysing CPN models. Using CPN Tools, it is possible to investigate the behaviour of the modelled system using simulation, to verify properties by means of state space methods and model checking, and toconduct simulation-based performance analysis. User interaction with CPN Tools is based on direct manipulation of the graphical representation of the CPN model using interaction techniques, such as tool palettes and marking menus. A license for CPN Tools can be obtained free of charge, also for commercial use.

Download author-created version of full paper (PDF) (755 KB)
© Springer
The original publication is available at http://www.springerlink.com, or via STTT in SpringerLink, or via DOI bookmark.

Errata for STTT version

1. Sect 2.1: "Packets ToSend" should be "PacketsToSend" in the paragraph starting with "The current marking".
2. Sect. 2.4, Fig. 13: The figure is incorrect because it is missing a token. The figure should be :
3. Sect. 2.4: "CPN tools" should be "CPN Tools" in the paragraph starting with "Each instance".
4. Sect. 3.1, Fig. 19: The figure is incorrect with respect to the statement "the Tool box entry has been opened to show its nine subentries (from Auxiliary to View)" in the paragraph starting "A small triangle". The upper left corner of the figure should look like this:
   
5. Sect. 3.1: "Declarations" should be "declarations" in the second and third lines of the paragraph starting with "The colour sets, variables"
6. Sect. 5.3: The line 1`"COLOURED PETRI" should be 1`"COLOURED PETRI " (i.e., there should be a space between the I and the ") just before the paragraph starting "This corresponds".
7. Sect. 5.3 "PacketToSend" should be "PacketsToSend" in the last line of the paragraph starting "The best lower multi-set bound".