Browse Books

Reviewer: Marian Gheorghe

Written within the scope of a European Union project, "Modelling and Analysis of Time Constrained and Hierarchical Systems," this book focuses on system modeling and verification in the context of Petri net-based modeling. It presents the results of cooperation of four Petri net research groups, from the universities of Eindhoven, Hamburg, Paris VI, and Zaragoza. Five parts comprise the book, demonstrating how Petri nets fill many of the needs of systems modeling, verification, and implementation. Part 1 seeks to define the Petri net model in an intuitive form. It introduces the basic concepts related to this model, such as locality and concurrency, graphical and algebraic representation, conflict and confusion, refinement and composition, and net morphisms. Through a number of simple examples, the concepts of place/transition nets and colored nets are presented. This part ends with a discussion of the basic properties of this model: reachability graphs, linear invariants, liveness, and reversibility. Part 2 presents different modeling aspects of Petri nets. Various application areas are illustrated using elementary nets, place/transition nets, or colored nets. Although it is well known that modeling is more of an art, a number of general principles of modeling using Petri nets are presented. The use of Petri nets within methods that support structural approaches for modeling, validating, and verification is illustrated by considering three perspectives: the state-oriented approach, the event-oriented view, and object-oriented modeling. For each method, a case study developing a mutual exclusion algorithm is provided. Part 3 is an overview of the main aspects of Petri net models verification. First, the state-based methods are described, demonstrating how the computation of the state space may be managed efficiently. Then, partial-order methods, symmetries, and modular methods are discussed. Finally, the model-checking problem is presented in general terms. Another view of verification, involving structural methods, is also discussed. The last part presents new techniques from an open research field. Part 4 is mainly dedicated to validation and execution; it will be of interest to systems engineers. This part discusses validation within the systems engineering area, and relates it to prototyping and tools. Different types of distributed execution concepts and their relevance are presented. Automatic code generation for distributed software systems from Petri nets is covered as well. The final part presents three in-depth studies. The focus is on three application domains: flexible manufacturing, workflow management, and telecommunications. Illustrative examples are used in the book, as well as a rigorous approach to successfully present the main problems related to system modeling and verification using the Petri net model. The book will mainly be useful to system engineers using Petri nets as a means of modeling their applications. Several tools are available to build Petri net models, to analyze their properties, and to validate them. Online Computing Reviews Service