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

TY - JOUR

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

AU - Jensen, Kurt

AU - Kristensen, Lars Michael

AU - Wells, Lisa Marie

PY - 2007

Y1 - 2007

N2 - Coloured Petri Nets (CPNs) is a language for the modeling and validation og systems in which concurrency, communication, and synchronisation play a major role. Coloured Petri Nets is a descrete-event modeling language combining Petri Nets with the funcitonal programming language Standard ML. Petri nets provide the doundation of the graphical notation and the basic primitives for modeling concurrency, communication, and synchronisation. Standard ML provides the primitives for the defintion of data types, describing data manipulation, and for creation compact and prarmeterisable models. A CPN model of a system is an executable model representing the states of the sytem and the events (transitions) that can cause the system to chande state. The CPN language makes it possicle to organise a model as a set of modules, and it includes a time concept that makes it possible to represent the time taken to execute events in the modelled system.CPN Tolls is an industrial-strength computer tool for construction 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 sp0ece methods and model checking, and to conduct simulation-based prerformace analysis. User interaction with CPN Tools is based on direct manipulation of the graphicla representation of the CPN model suing interaction techniques, such as tool palettes and maring menus. The functionality of the tool can be extended with user-defined Standard ML functions. A license for CPN Tools can be obtained free of charge, also for commercial use.

AB - Coloured Petri Nets (CPNs) is a language for the modeling and validation og systems in which concurrency, communication, and synchronisation play a major role. Coloured Petri Nets is a descrete-event modeling language combining Petri Nets with the funcitonal programming language Standard ML. Petri nets provide the doundation of the graphical notation and the basic primitives for modeling concurrency, communication, and synchronisation. Standard ML provides the primitives for the defintion of data types, describing data manipulation, and for creation compact and prarmeterisable models. A CPN model of a system is an executable model representing the states of the sytem and the events (transitions) that can cause the system to chande state. The CPN language makes it possicle to organise a model as a set of modules, and it includes a time concept that makes it possible to represent the time taken to execute events in the modelled system.CPN Tolls is an industrial-strength computer tool for construction 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 sp0ece methods and model checking, and to conduct simulation-based prerformace analysis. User interaction with CPN Tools is based on direct manipulation of the graphicla representation of the CPN model suing interaction techniques, such as tool palettes and maring menus. The functionality of the tool can be extended with user-defined Standard ML functions. A license for CPN Tools can be obtained free of charge, also for commercial use.

KW - Coloured Petri Nets

KW - Behavioural Modelling

KW - Simulation

KW - Verification

KW - State Space Methods

KW - Model Checking

KW - Performance Analysis

KW - Visualisation

U2 - 10.1007/s10009-007-0038-x

DO - 10.1007/s10009-007-0038-x

M3 - Journal article

SN - 1433-2779

VL - 9

SP - 213

EP - 254

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 3/4

ER -