This booklet contains the proceedings of the Fourth Workshop on Practical Use of Coloured Petri Nets and the CPN Tools, August 28-30, 2002. The workshop is organised by the CPN group at the Department of Computer Science, University of Aarhus, Denmark.

Coloured Petri Nets and the CPN Tools are now licensed to more than 7,200 users in 138 countries. The aim of the workshop is to bring together some of the users and in this way provide a forum for those who are interested in the practical use of Coloured Petri nets and their tools. The submitted papers were evaluated by a programme committee with the following members:

Wil van der Aalst, Netherlands

João Paulo Barros, Protugal

Jörg Desel, Germany

Joao M. Fernandes, Portugal

Jorge de Figueiredo, Brazil

Monika Heiner, Germany

Kurt Jensen, Denmark (chair)

Ekkart Kindler, Denmark

Lars M. Kristensen, Denmark

Charles Lakos, Australia

Johan Lilius, Finland

Daniel Moldt, Gremany

Laure Petrucci, France

Rüdiger Vlak, Germany

Lee Wagenhals, USA

Karsten Wolf, Germany

Jianli Xu, Finland

The programme committee has accepted 10 papers for presentation. Most of these deal with different projects in which Coloured Petri Nets and their tools have been put to practical use -- often in an industrial setting. The remaining papers deal with different extensions of tools and methodology.

The papers from the first eight CPN Workshops can be found via web pages: http://www.daimi.au.dk/CPnets/. After an additional round of reviewing and revision, some of the papers have been published in four special sections in the International Journal on Software Tools for Technology Transfer (STTT). For more information see: www.sttt.cs.uni-dortmund.de/. After an additional round of reviewing and revision, some of the papers from this years workshop will be published in Transactions of Petri Nets and Other Models of Concurrency (ToPNoC) which is new journal subline of Lecture Notes in Computer Science. For more information see: www.springer.com/lncs/topnoc.

Kurt Jensen

PC and OC chair

-- Languages based on nets.

-- The problem of time in nets.

-- Nets and related models.

-- Nets and formal semantics.

-- Parallel program verification and nets.

Delta is a language designed for general system description. It is partly build upon Simula, but is more than a programming language, since it contains several features, which cannot be implemented on a computer system. E.g. a continuous time concept, concurrency between an unbounded number of components and the possibility of using predicates to specify state changes.

In this paper a formal semantics for Delta is defined and analysed using Petri nets.

Petri nets was chosen because the ideas behind Petri nets and Delta concide on several points.

A number of proposals for changes in Delta, which resulted from this work, are also reported here, whereas a number of different extensions to the Petri net formalism may be found in (DAIMI TR-5).

I have edited the material provided by the original authors. I have modified some of the CP-nets, e.g., to improve the layout and use more mnemonic names. In some cases, I have also changed a few net components, e.g., merged two transitions or introduced a Standard ML function for operations that are used in many arc expressions. These modifications make the CP-nets more appropriate as study material, but they do not change the essential behaviour of the CPN models.

The terminology in the original material has been modified to fit the terminology introduced in the first two volumes of this book. Redundancies with the material of the other volumes have been removed, e.g., the explanation of what a hierarchical CP-net is and how the CPN tools work. The typography has been modified to match that used for the other parts of the book. More detailed explanations have been added, e.g., of some of the CPN models and some of the analysis results. This has been possible since, Vols. 1 and 2 have given the readers a much more thorough knowledge of CP-nets than readers of ordinary research papers. Finally, it is discussed how some of the problems from the projects can be overcome or circumvented. Many of these problems have already been removed, e.g., by improvements of the CPN tools. Other problems can be avoided by a careful choice of modelling and analysis techniques.

The material has been modified in cooperation with the original authors and the final result has been approved by them. The conclusions and findings of the original papers have not been modified.

The CPN tools for occurrence graphs and performance analysis are rather new compared to the CPN editor and simulator. Nevertheless, they have been successfully used by several of the industrial projects reported in this volume. For place and transition invariants there is not yet adequate tool support, and hence they are much more infrequently used in practical projects.

We define state spaces and condensed state spaces for a language called Coloured Petri Nets (CP-nets). This language is in widespread use for the modelling and analysis of concurrent systems. However, our techniques are general and they can be used for many other kinds of labelled transition systems. The paper does not assume that the reader is familiar with CP-nets (or Petri nets in general) - although such knowledge will, of course, be a help. The first four sections of the paper introduce the basic concepts of CP-nets. The next three sections deal with state spaces, condensed state spaces and computer tools for state space analysis. Finally, there is a short conclusion.

In this textbook, Jensen and Kristensen introduce the constructs of the CPN modelling language and present the related analysis methods in detail. They also provide a comprehensive road map for the practical use of CPN by showcasing selected industrial case studies that illustrate the practical use of CPN modelling and validation for design, specification, simulation, verification and implementation in various application domains.

Their presentation primarily aims at readers interested in the practical use of CPN. Thus all concepts and constructs are first informally introduced through examples and then followed by formal definitions (which may be skipped). The book is ideally suitable for a one-semester course at an advanced undergraduate or graduate level, and through its strong application examples can also serve for self-study. It features an accompanying website that offers additional material such as slides, exercises and project proposals.