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 -