LSCS 01: Petri Net Approaches for Modelling and Validation

Petri Net Approaches for Modelling and Validation

Wil van der Aalst, José-Manuel Colom, Fabrice Kordon, Gabriela Kotsis & Daniel Moldt


The successful realization of complex systems of interacting and reactive software and hardware components relies heavily on the use of a precise language at different stages of the development process. Petri nets are becoming increasingly popular in this area, as they provide a uniform language supporting the tasks of modelling, verification, and validation. Their popularity is due to the fact that fundamental aspects of causality, concurrency, and choice are captured by Petri nets in a natural and mathematically precise way without compromising readability.

Several methods, techniques, tools, and algorithms have been developed to ease the practical work and support the basic ideas behind the usage of Petri nets in the area of system engineering. However, this does not mean that complete and ready to use systems and approaches are available or even established. Therefore, a general understanding of the potentials of Petri nets in the context of system engineering needs to be provided and distributed.

The workshop "Petri Nets in System Engineering" (PNSE'97) was held at the Department of Computer Science, University of Hamburg on September 25--26, 1997. It brought together experts from the communities of Petri nets and system engineering both from industry and academia to exchange the newest results and experiences. The workshop was organized by the members of the European community project MATCH (Modelling and Analysis of Time Constrained and Hierarchical Systems). Project partners include the universities of Eindhoven, Genova, Hamburg, Paris, Turin, Vienna, and Zaragoza. This post-workshop book puts together some papers presented at the workshop which were rewritten and then selected after a second reviewing process. The selected approaches cover modelling, verification, and validation. They provide an insight into new ideas of modelling and validation with modules or objects and a comparison of event- and state-based modelling. Some contributions explain verification techniques based on state spaces and temporal logic. This allows event- and state-based specification and verification. Furthermore, the analysis of systems by structural techniques is covered as well as feasibility of using Petri nets and related tools for the analysis of workflows. Altogether the papers reflect current and relevant research and work on Petri nets in system engineering.

Contents: W.M.P. van der Aalst: Putting Petri Nets to Work in the Workflow Arena. S. Christensen, L.M. Kristensen: State Space Analysis of Hierarchical Coloured Petri Nets. O. Fricke: Data Abstraction in Petri Nets as Modular Structuring Concept. F. Garcia-Valles, J.M. Colom: Structural Analysis of Signal Transition Graphs based on Linear Algebra Techniques. J.B. Jorgensen, L.M. Kristensen: Verification of Coloured Petri Nets Using State Spaces with Equivalence Classes. E. Kindler, T. Vesper: ESTL: Some Proof Techniques. R. Mackenthun, M. Voorhoeve: Modelling and Verification with Petri Nets. Ch. Maier, D. Moldt: Dynamic Structure and Behaviour of Coloured Petri Nets Supporting Object-Oriented Modelling.

ISBN 9783895865978. LINCOM Studies in Computer Science 01. 143pp. 2003.