Coloured Petri Nets and CPN Tools for Modelling and
Validation of Concurrent Systems
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 to conduct 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.
Keywords: Introduction to CP-nets, Simulation, State spaces, Occurrence graphs, CP-nets with time,
Hierarchical CP-nets, Tool support, Application, General.
Modification Date?