The practitioner's guide to coloured Petri nets
International Journal on Software Tools for Technology TransferPublished 1 December 1998
Lars Michael Kristensen, Søren Christensen, Kurt Jensen
Citations314
SJR quartileQ3
SJR score0.38
SNIP1.13
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This paper provides a comprehensive road map to the practical use of Petri nets and the Design/CPN tool and gives an informal introduction to the basic concepts and ideas underlying CP-nets.
Abstract
Coloured Petri nets (CP-nets or CPNs) provide a framework for the desing, specification, validation, and verification of systems. CP-nets have a wide range of application areas and many CPN projects have been carried out in industry, e.g., in the areas of communication protocols, operating systems, hardware design, embedded systems, software system designs, and busness process-engineering. Design/CPN is a graphical computer tool supporting the practial use of CP-nets. The tool supports the construction, simulation, and functional and performance analysis of CPN models. the tool is used by more than four hundred commercial companies. It is available free of charge, also for commercial use. This paper provides a comprehensive road map to the practical use of CP-nets and the Design/CPN tool. We give an informal introduction to the basic concepts and ideas underliying CP-nets. The key components and facilities of the Design/CPN tool are presented and their use illustrated. The paper is self-contained and does not assume any prior kowledge of Petri nets and CP-nets nor any experience with the Design/CPN tool
Keywords
Computer Science
Proceedings of the IEEEPetri nets: Properties, analysis and applications
10,546 Citations1989T. Murata
The author proceeds with introductory modeling examples, behavioral and structural properties, three methods of analysis, subclasses of Petri nets and their analysis, and one section is devoted to marked graphs, the concurrent system model most amenable to analysis.
ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications
3,555 Citations1986E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems.
Lecture notes in computer scienceSymbolic model checking
2,843 Citations1996Emma L. Clarke, K. McMillan +2 more
Using symbolic model checking techniques it is possible to verify industrial-size finite state systems and models with more than 10120 states have been verified using special techniques.
The MIT Press eBooksThe Definition of Standard ML
2,411 Citations1997Robin Milner, Robert Harper +2 more
This book provides a formal definition of Standard ML for the benefit of all concerned with the language, including users and implementers, and the authors have defined their semantic objects in mathematical notation that is completely independent of StandardML.
Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use
2,007 Citations2011Kurt Jensen
Design and validation of computer protocols
1,695 Citations1991Gerard J. Holzmann
Part 1 Basic: introduction protocol structure error control flow control and design tools: a protocol simulator a protocol validator using the validator.
ACM SIGMETRICS Performance Evaluation ReviewModelling with Generalized Stochastic Petri Nets
1,384 Citations1998Marco Ajmone Marsan, Gianfranco Balbo +3 more
This book presents a unified theory of Generalized Stochastic Petri Nets together with a set of illustrative examples from different application fields to show how this methodology can be applied in a range of domains.
Algorithmic graph theory
830 Citations1985Alan Gibbons
Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem
771 Citations1996Patrice Godefroid, Jan Van Leeuwen +3 more
Formal Methods in System DesignA stubborn attack on state explosion
572 Citations1992Antti Valmari
The LTL-preserving stubborn set method is presented for reducing the amount of work needed in the automatic verification of concurrent systems with respect to linear-time temporal logic specifications.
The SGML handbook
544 Citations1990Charles F. Goldfarb
This paper introduces generalized markup, a model for generalized markup that automates the very labor-intensive and therefore time-heavy and expensive process of developing and distributing SGML documents.
Lecture notes in computer scienceAll from one, one for all: on model checking using representatives
521 Citations1993Doron Peled
An algorithm for constructing a state graph that contains at least one representative sequence for each equivalence class, and a formula rewriting technique is presented to allow coarser equivalence relation among sequences, such that less representatives are needed.
Formal Methods in System DesignBetter verification through symmetry
491 Citations1996C. Norris Ip, David L. Dill
This work provides a proof of the soundness of the new symmetry-based verification algorithm based on a definition of the formal semantics of a simple description language with scalarsets, and leads to an alternative characterization of data independence.
Cambridge University Press eBooksML for the Working Programmer
489 Citations1996Laurence C. Paulson
In teaching the methods of functional programming, how to program in Standard ML, a functional language recently developed at Edinburgh University, the author shows how to use such concepts as lists, trees, higher-order functions and infinite data structures.
Lecture notes in computer scienceColoured Petri Nets
476 Citations1987Kurt Jensen
This is the third volume of a definitive work on coloured Petri nets and contains a detailed presentation of 19 applications of CP-nets across a broad range of application areas, including a security system, ATM networks, audio/video systems, transaction processing, ISDN services, VLSI chips, document storage, distributed programming, electronic funds transfer, and many more.
Formal Methods in System DesignSymmetry and model checking
386 Citations1996E. Allen Emerson, A. Prasad Sistla
This work shows how to exploit symmetry in model checking for concurrent systems containing many identical or isomorphic components, and focuses in particular on those composed of many isomorphic processes.
Formal Methods in System DesignProperty preserving abstractions for the verification of concurrent systems
357 Citations1995Claire Loiseaux, Susanne Graf +4 more
Results are given on the preservation of properties expressed in sublanguages of the branching time μ-calculus when two systemsS andS' are related via (α, γ)-simulations, using simulations parameterized by Galois connections.
Lecture notes in computer scienceUsing partial orders to improve automatic verification methods
285 Citations2005Patrice Godefroid
Lecture notes in computer scienceStandard ML of New Jersey
245 Citations1991Andrew W. Appel, David MacQueen
The Standard ML of New Jersey compiler has been under development for five years now and has developed a robust and complete environment that supports the implementation of large software systems and generates efficient code.
Medical Entomology and ZoologyElements of Ml Programming
199 Citations1994Jeffrey D. Ullman
A perspective on ML and SML/NJ and how to program with Datatypes and Solutions to Selected Exercises are presented.
Lecture notes in computer scienceAn introduction to the practical use of coloured Petri Nets
152 Citations1998Kurt Jensen
The development of Coloured Petri Nets has been driven by the desire to develop a modelling language theoretically well-founded and versatile enough to be used in practice for systems of the size and complexity found in typical industrial projects.
DAIMI Report SeriesAn Introduction to the Theoretical Aspects of Coloured Petri Nets
125 Citations1994Kurt Jensen
DAIMI Report SeriesModel Checking Coloured Petri Nets - Exploiting Strongly Connected Components
80 Citations1997Allan Cheng, Søren Christensen +1 more
A CTL-like logic which is interpreted over the state spaces of Coloured Petri Nets, designed to express properties of both state and transition information and a model checking algorithm which for efficiency reasons utilises strongly connected components and formula reduction rules.
ACM SIGCOMM Computer Communication ReviewBook Review: Design and Validation of Computer Protocols by Gerard J. Holzmann (Prentice Hall, 1991)
69 Citations1991Lars‐Åke Fredlund
The author presents the contents of a protocol specification, and describes basic rules for constructing protocols successfully, and uses reachability analysis methods to verify that a protocol satisfies each type of correctness criterion.
Theoretical Computer ScienceReachability trees for high-level petri nets
64 Citations1986Peter Huber, Arne M. Jensen +2 more
A generalization of reachability trees is contributed to, which is one of the other important analysis methods known for place/transition nets.
Lecture notes in computer scienceDesign/CPN — A computer tool for Coloured Petri Nets
57 Citations1997Søren Christensen, Jens Bæk Jørgensen +1 more
The computer tool Design/CPN is described, supporting editing, simulation, and state space analysis of Coloured Petri Nets in the design, validation, and verification of communication protocols for audio/video systems.
Lecture notes in computer scienceModular state space analysis of coloured Petri Nets
41 Citations1995Søren Christensen, Laure Petrucci
State Space Analysis is one of the most developed analysis methods for Petri Nets but cannot yet handle industrial size systems.
Lecture notes in computer scienceCompositionality in state space verification methods
34 Citations1996Antti Valmari
The concepts and ideas that are necessary for understanding computerised process-algebraic compositional verification are introduced and some advanced ways of using the basic techniques are described.
Lecture notes in computer scienceDesigning a security system by means of Coloured Petri Nets
32 Citations1996J L Rasmussen, Mejar Singh
An animation utility was developed which made it possible to perform user-friendly CP-net simulations and occurrence graphs were used for debugging the CP-nets, reducing the amount of errors in the final implementation.
Lecture notes in computer scienceFinding Stubborn Sets of Coloured Petri Nets without Unfolding
27 Citations1998Lars Michael Kristensen, Antti Valmari
A lower bound result is given stating that there exist CP-nets for which computing "good" stubborn sets requires time proportional to the size of the equivalent PT-net, and an approximative method is suggested which does not rely on unfolding.
IEEE Transactions on Parallel and Distributed SystemsComputer aided verification of Lamport's fast mutual exclusion algorithm using colored Petri nets and occurrence graphs with symmetries
23 Citations1999Jens Bæk Jørgensen, Lars Michael Kristensen
A computer tool is presented that implements the method of occurrence graphs with symmetries (OS-graphs) for Colored Petri Nets (CP-nets) and demonstrates a significant increase in the number of states which can be analyzed.
Lecture notes in computer scienceDesigning and verifying a communications gateway using coloured Petri nets and design/CPN™
21 Citations1996Daniel Floreani, Jonathan Billington +1 more
A gateway between a packet radio network and B-ISDN is being designed as part of a larger project that aims to bring modem telecommunications services to the Australian Defence Force.
Lecture notes in computer scienceAnalysis of an Ada system using coloured Petri nets and occurrence graphs
21 Citations1992William W. McLendon, Richard F. Vidale
This paper summarizes a project that used a new prototype occurrence graph (OG) tool to analyze a hierarchical coloured Petri net, and believes the approach can, with further refinements, become a practical means of verifying Ada program designs.
Lecture notes in computer scienceFormal verification of an arbiter cascade
20 Citations1992Hartmann J. Genrich, Robert M. Shapiro
This work uses a hierarchical Colored Petri Net to describe the arbiter circuit and the protocol for using it, and describes the layout of a 2d input cascade of (2d-1) arbiters, d≥1 being the depth of the cascade.
International Journal on Software Tools for Technology TransferAnalysis and verification of real-time systems using quantitative symbolic algorithms
18 Citations1999S x E rgio Vale Aguiar Campos, Edmund M. Clarke
The technique evaluates how well the system works or how seriously it fails, as opposed to only whether it works or not, which demonstrates that the method proposed is efficient enough to be used in real-world designs.
On scalable net modeling of OLTP
12 Citations2002Ludmila Cherkasova, V. E. Kotov +1 more
The goal was to propose a convenient and flexible model that would be easy to modify with respect to different scheduling algorithms, number of processors, and disks and exploit the scalability of colored Petri nets.
Lecture notes in computer scienceModelling the work flow of a nuclear waste management program
11 Citations1994Kjeld Høyer Mortensen, Valerio O. Pinci
A modelling project to improve a nuclear waste management program in charge of the creation of a new system for the permanent disposal of nuclear waste is described.
Lecture notes in computer scienceVisualising the behaviour of intelligent networks
9 Citations1998Carla Capellmann, Søren Christensen +1 more
This paper shows how designers of services in an Intelligent Network can use Coloured Petri Nets to obtain a description of the services which on the one hand is precise and unambiguous, and on the other hand provides the basis for a comprehensive and thorough understanding of the behaviour by visualising the processes.
Lecture notes in computer scienceSimulation and analysis of a document storage system
8 Citations1994Gert Scheschonk, Michael Timpe
The goal of this project was to develop a model of the critical parts of the system in order to identify bottlenecks and to find the right scaled hardware configuration.