Petri Nets E-Book

• Herausgeber: John Wiley & Sons
• Kategorie: Wissenschaft und neue Technologien
• Sprache: Englisch

Seitenzahl: 991

Veröffentlichungsjahr: 2013

Beschreibung

A Petri net is a mathematical representation of a network. This book first introduces the basic models including time and stochastic extensions, in particular place-transition and high level Petri nets. Their modeling and design capabilities are illustrated by a set of representations of interest in operating and communication systems. The volume then addresses the related verification problems and proposes corresponding solutions by introducing the main notions needed to fully understand the behavior and properties behind Petri nets. Particular attention is devoted to how systems can be fully represented and analyzed in terms of their behavioral, time, and stochastic aspects by using the same formal approach and semantic basis. Finally, illustrative examples are presented in the important fields of interoperability in telecommunication services, programming languages, multimedia architectures, manufacturing systems, and communication protocols.

Leseprobe

Table of Contents

Preface

Introduction

Part 1 Fundamental Models

Chapter 1 Basic Semantics

1.1. Automata or state machines

1.2. State machines and Petri nets (PN)

1.3. Concepts and definitions

1.4. Accessibility graph or marking graph

1.5. Some basic models

1.6. Conclusion

1.7. Bibliography

Chapter 2 Application of Petri Nets to Communication Protocols

2.1. Basic models

2.2. A simple establishment of a connection

2.3. The alternating bit protocol (ABP): model and verification

2.4. Communicating state machines and PNs

2.5. Conclusion

2.6. Bibliography

Chapter 3 Analysis Methods for Petri

3.1. Introduction

3.2. Behavioral analysis of Petri nets

3.3. Analysis of nets by linear invariants

3.4. Net reductions

3.5.The graph of a Petri net

3.6. Bibliography

Chapter 4 Decidability and Complexity of Petri Net Problems

4.1. Introduction

4.2. Decidability and complexity notions

4.3. Theoretical results about the reachability graph

4.4. Analysis of unbounded Petri nets

4.5. The reachability problem

4.6. Extensions of Petri nets

4.7. Languages of Petri nets

4.8. Bibliography

Chapter 5 Time Petri Nets

5.1. Introduction

5.2. Time Petri nets

5.3. Behavior characterization – state classes' method

5.4. Analysis – operating the state class graph

5.5. Application example

5.6. Extensions and variations

5.7. Implementation using the Tina tool

5.8. Conclusion

5.9. Bibliography

Chapter 6 Temporal Composition and Time Stream Petri Nets

6.1. Time, synchronization and autonomous behaviors

6.2. Limitation of time PNs

6.3. Temporal composition

6.4. Temporal composition and temporal synchronization

6.5. Time stream PNs

6.6. Application to multimedia systems

6.7. Conclusion

6.8. Bibliography

Chapter 7 High Level Petri Nets

7.1. Introduction

7.2. Informal introduction to high level nets

7.3. Colored net definition

7.4. Well-formed net definition

7.5. Other high level formalisms

7.6. Conclusion

7.7. Bibliography

Chapter 8 Analysis of High Level Petri Nets

8.1. Introduction

8.2. The symbolic reachability graph

8.3. Colored invariants

8.4. Structural reductions

8.5. Conclusion

8.6. Bibliography

Chapter 9 Stochastic Petri Nets

9.1. Introduction

9.2. A stochastic semantics for discrete event systems

9.3. Stochastic Petri nets

9.4. Some standard analysis methods

9.5. Conclusion

9.6. Bibliography

Chapter 10 Stochastic Well-formed Petri Nets

10.1. Introduction

10.2. Markovian aggregation

10.3. Presentation of stochastic well-formed Petri nets

10.4. From the symbolic graph to Markovian aggregation

10.5. Conclusion

10.6. Bibliography

Chapter 11 Tensor Methods and Stochastic Petri Nets

11.1. Introduction

11.2. Synchronized Markov chains

11.3. Tensor algebra and SPN

11.4. Tensor decomposition of stochastic well-formed Petri nets

11.5. Conclusion

11.6. Bibliography

Part 2. Verification and Application of Petri Nets

Chapter 12 Verification of Specific Properties

12.1. Introduction

12.2. Kripke structures and transitions systems

12.3. Temporal logic

12.4. Behavioral approach

12.5. Decidability of bisimulation and of evaluation of formulas

12.6. Bibliography

Chapter 13 Petri Net Unfoldings – Properties

13.1. Introduction

13.2. Elementary concepts

13.3. Branching processes and unfoldings

13.4. Finite prefixes

13.5. Conclusion

13.6. Bibliography

Chapter 14 Symmetry and Temporal Logic

14.1. Introduction

14.2. Principles of the dynamic symmetry method

14.3. Illustration of the dynamic symmetry method

14.4. Efficient implementations and further work

14.5. Conclusion

14.6. Bibliography

Chapter 15 Hierarchical Time Stream Petri Nets

15.1. Introduction

15.2. Structured time stream Petri nets

15.3. Combining abstraction and temporal composition

15.4. Examples

15.5. Conclusion

15.6. Bibliography

Chapter 16 Petri Nets and Linear Logic

16.1. Introduction

16.2. Linear logic

16.3. Petri nets and linear logic

16.4. Sequent labeling and graph of precedence relations

16.5. Temporal evaluation of scenarios

16.6. Conclusion

16.7. Bibliography

Chapter 17 Modeling of Multimedia Architectures: the Case of Videoconferencing with Guaranteed Quality of Service

17.1. Introduction

17.2. Problems of multimedia synchronization

17.3. Modeling of multimedia synchronization constraints

17.4. Modeling of a synchronization architecture

17.5. Conclusion

17.6. Bibliography

Chapter 18 Performance Evaluation in Manufacturing Systems

18.1. Introduction

18.2. Modeling of manufacturing systems

18.3. Evaluation of manufacturing systems

18.4. Optimization of manufacturing systems

18.5. Conclusions

18.6. Bibliography

Conclusion

List of Authors

Index

First published in France in 2001 and 2003 by Hermes Science/Lavoisier entitled Les réseaux de Petri and Vérification et mise en œuvre des réseaux de Petri © Hermes Science Ltd, 2001 © LAVOISIER 2003

First published in Great Britain and the United States in 2009 by ISTE Ltd and John Wiley & Sons, Inc.

Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form or by any means, with the prior permission in writing of the publishers, or in the case of reprographic reproduction in accordance with the terms and licenses issued by the CLA. Enquiries concerning reproduction outside these terms should be sent to the publishers at the undermentioned address:

ISTE Ltd

John Wiley & Sons, Inc.

27-37 St George’s Road

111 River Street

London SW19 4EU

Hoboken, NJ 07030

UK

USA

www.iste.co.uk

www.wiley.com

© ISTE Ltd, 2009

The rights of Michel Diaz to be identified as the author of this work have been asserted by him in accordance with the Copyright, Designs and Patents Act 1988.

Library of Congress Cataloging-in-Publication Data

Réseaux de Petri and vérification et mise en œuvre des réseaux de Petri. English   Petri nets : fundamental models, verification, and applications / edited by Michel Diaz.       p. cm.   Includes bibliographical references and index.   ISBN 978-1-84821-079-0  1. Electronic data processing--Distributed processing. 2. Parallel processing (Electronic computers) 3. System design. 4. Petri nets. I. Diaz, Michel, 1945- II. Title.   QA76.9.D5P4813 2009   511.3'5--dc22

2009017412

British Library Cataloguing-in-Publication Data

A CIP record for this book is available from the British Library

ISBN 978-1-84821-079-0

Preface

Future advanced architectures, such as embedded systems, having a greater complexity and new quality requirements, will need a more precise specification and better control of their design process. In order to acquire the corresponding fundamental knowledge, it is essential to rely upon approaches based on the use of adequate system models. In particular, such approaches need to acquire a deep understanding of the system, including its local behaviors and its communications, based on a well-defined representation of the designed architecture. This representation should be used as early as possible to analyze and validate the design. The goal of this volume is to present a family of formal specification models, based on Petri nets and extensions of Petri nets, because they are defined by simple and clear semantics, allow easy modeling of system key mechanisms, and are supported by strong analysis methods and tools. Furthermore, this set of models can be used for all design aspects, i.e. to specify functional behaviors, and to include temporal or stochastic requirements.

The main results related to this approach are given in this volume, in two parts, one presenting the fundamental models, and the other being dedicated to verification and applications. We have tried to highlight the important characteristics and the main properties of these models, and to show how they lead to the emergence of a full design methodology, which is both complete, in terms of all possible functional and other analysis, and integrated, because the same basic semantics are used for the full design support. We think that this volume should greatly help any designer to build the new forthcoming generation of distributed systems.

Lastly, I would like to thank all the authors who contributed to this book, for their expertise, their seriousness, their technical inputs, and for the great job they have done.

Michel DIAZ

Introduction

New technologies in processors and networks allow system designers to conceive and build advanced and sophisticated parallel and distributed architectures, which need to integrate non-functional real time and stochastic constraints with functional distributed processing and communication.

The global behavior of such systems depends first on the local activities and data, but also on the messages sent and received by the various interconnected subsystems. As a matter of fact, understanding, expressing, specifying and validating such global behaviors proves to be a problem of very high complexity, leading to many design and implementation difficulties and bugs. For example, when considering n connected processors, they can run, at a given instant in time, using 2 x 2, 3 x 3 communications, etc., or a full communication, in which all n processors interact. The sum of the resulting combinations, of the order of 2n, shows the complexity of the resulting conceptual problems, and explains in particular the increasing difficulty obtained when passing from an interconnection of a few processors to an interconnection of a large number of processors: when the number of processors varies from 2 to 10, the difficulty coefficient goes from 4 to about 1,000.

It should then be clearly understood that designing such distributed architectures leads to a very complex conceptual task, which has to be based on a well-defined methodology to be able to manage all system requirements and behaviors.

Design and specification

The design process starts by giving the different functions and agents which are required, and the way they are structured; second, the designers define the behaviors of the various processes and entities, and the way they communicate; then, if they want to analyze the correctness of the design as soon as possible, an adequate approach is needed to represent, in an explicit way, the (full) system global behavior, in particular to be able to check potential unanticipated sub-behaviors.

To check the design correctness, it is essential to use a precise model of all critical mechanisms, functions, sub-systems, etc., and then, whenever possible, to use a formal model, to define a mathematical representation of the system. Checking the correctness validation of the design at this step is then conducted by checking the behavior of this system model.

Note that, after a given adequate sequence of more or less formal validation steps based on models, the system will be defined as ‘fully designed’ and will be implemented using adequate tools and languages.

Formal approaches have been used for many years for the verification of communication protocols. Two principal approaches have been used., i.e. basic formal models, such as automata, Petri nets, process algebras, etc., and formal description techniques for protocols, such as Estelle, LOTOS, SDL, etc.

This volume proposes and develops a design and validation methodology that relies on the use of a family of basic formal models that are rather easy to understand, and able to:

– describe the semantics of all basic building mechanisms;

– clearly specify the interconnection and communication semantics;

– unambiguously describe the resulting behaviors;

– validate the system during the first phases of its design by using support tools.

In general, basic non-language oriented graphical models, that do not include language-specific operators and statements, lead to the simplest solutions for representing basic mechanisms in a very abstract and integrated way.

For this reason too, this volume selected a basic, language-independent set of models to represent and manipulate the fundamental concepts of communicating architectures.

Selecting a model

Several models exist, and each model has particular characteristics, more or less relevant for a specific design. Consequently, the choice of the right model depends on the designed system and on the properties to be analyzed, as the model must be able to describe the design, and also to allow the designer to check the validity of the required properties.

In general, the designer must have a good understanding of the fundamental semantics of the system, i.e. of its basic building mechanisms. Thus, for simple architectures, modeling will be able to represent in a faithful way all details of the system. However, for complex systems, it will generally be impossible, for economic reasons, to represent the details of all existing functions, and it will become necessary to select and validate certain building blocks, i.e those most likely to lead to erroneous behaviors.

Of all existing models, Petri nets (PN) and their extensions are of undeniable fundamental interest, because they:

– provided the first modeling approaches for the semantics of concurrent systems, and were used to model the behaviors of the first parallel and distributed basic mechanisms;

– define easy graphic support for the representation and the understanding of these basic mechanisms and behaviors;

– prove to be, starting from state machines, an easy extension of previous approaches and handle, at the same time, the creation and the analysis of models;

– express very simply the main basic concepts in communication, including waiting and synchronization, and furthermore take into account their temporal and stochastic parameters;

– ensure, being unrelated to a particular implementation language, the independence of the specification with respect to its implementation.

Furthermore, many validation methods have been developed, using a great number of theoretical results and support tools, able to manipulate functional, temporal, and stochastic behaviors. Finally, models based on PNs will help us to understand, define and analyze the behavior of these systems, in the preliminary and first steps of their design.

For all these reasons, a set of Petri net models was selected in this book to represent and manipulate the fundamental concepts of communicating architectures.

Petri nets

PNs were introduced by A.C. Petri in 1962 to synchronize communicating automata, and were then extended to define a large set of models, with increasing complexity and capabilities.

As will be seen, this family of PNs, starting from the simple traditional state machines, now allows system designers to handle in an integrated way the functional (qualitative) and the non-functional (e.g. quantitative) temporal and stochastic capabilities of systems.

Extensions of PNs were proposed according to two important axes:

a)  for qualitative properties and behaviors, to use simpler and more compact models, by high level PNs, for handling generic behaviors (e.g. individual) and data, predicates and functions;

b)  complementing this first axis, for quantitative properties and behaviors, to extend the previous models by integrating quantitative constructs and parameters related to temporal and stochastic requirements.

It is significant to note that all first and conceptual studies in these quantitative fields were carried out using PN-based models.

Functional qualitative properties

The first PN model, called the Condition–Event PN, was based on the use of Boolean values: true or false. It was generalized by Place–Transition PNs, now simply called PNs, which can use integers. This volume will begin with their presentation and validation.

Non-functional quantitative properties

The fundamental contributions of the second axis considers:

– time PNs, or TPNs, used for systems whose behaviors depend explicitly on temporal values;

– stochastic PNs, or SPNs, for which distributions are attached to the model, in particular for performance evaluation and reliability.

Families of PNs

When applied to the modeling of systems, it rapidly becomes apparent that these models do not have the same application power, in terms of:

– definition and description of the concepts for parallelism, distribution, and synchronization;

– understanding and using the temporal and stochastic semantics;

– analyzing the possibly different mechanisms and behaviors, in very different contexts and applications.

Figure 1 represents some of the principal models of this family. In this figure, an arrow means that the model at the end of the arrow was proposed after the model at the beginning of the arrow, and so gives the steps followed by the research to propose and develop these principal PN-based models.

Figure 1.The main Petri net models

Figure 2 gives a more conceptual view of these models, by clarifying their syntactic and semantic relationships. In this figure, three fields are respectively defined by:

– a discrete state semantics, for non-temporal and non-stochastic nets, behaviors being represented by a finite graph of all model states;

– a semantics on continuous time, for extended behaviors based on dense time models;

– and stochastic semantics, for behaviors including distributions.

Let us emphasize that these models have three models of reference, respectively PN, TPN, and SPN. Moreover, each model is a pure extension of a previous one, as it can by simplified to become a basic PN model.

As seen in the figure, the models derived from the reference models:

– lead to more compact models, i.e. are abbreviations, that do not increase the expressiveness of the model, but simplify the model and the system specification;

– or are more powerful in terms of expressive power, i.e. are able to describe mechanisms which could not be described by the unextended models (e.g. introducing time parameters, stochastic distributions, etc., for real-time or dependable systems).

Figure 2.Semantics domains of the Petri net-based models

For example:

– PN led to PN with inhibitor arcs (to test the presence of zero token in one

place), PN with reset arcs, etc.;

– TPN led to TPN with streams to compose and synchronize independent behaviors with independent temporal constraints, etc.;

– SPN led to SPN with immediate transitions in order to manage the case where transition cannot be delayed, etc.

Consequently, many different models exist, of different power and for different fields of application, but they follow the same semantics basis, and will allow the designers to carry out coherent complementary analyses to validate the correct operation of the modeled (and designed) systems.

The semantics of these models and their properties were used to select, define, and study the most important members of the PN family in the two parts of this volume.

Table of contents of the volume

Part 1 is dedicated to fundamental models and contains 11 chapters. Part 2 addresses verification and applications, and contains the last 7 chapters.

Part 1

Chapter 1 introduces Place–Transition PNs, more simply called Petri Nets (PNs). It gives their fundamental definitions, presents some basic models and clarifies their interest.

Chapter 2 illustrates an application in a very important area: communication protocols; simple PN examples show at the same time the power of the model and the interest of the formal analysis.

Chapter 3 first introduces the general properties that can be checked using PNs (blocking, reachability or accessibility, etc.) and the verification approach that uses the graph of the reachable (or accessible) states. The set of reachable (or accessible) states is the set of states that are reachable or accessible from a given initial state. Two optimization methods of analysis are then presented, one based on linear algebra techniques, and the other one exploiting the topological structure of the PNs.

Chapter 4 deals with the decidability and complexity problems related to checking these general properties.

Chapters 5 and 6 consider models and behaviors based on explicit values of time, and show how to model temporal mechanisms.

Chapter 5 presents the general model, Time PN or TPN, which associates a given interval (minimum, maximum) to each transition; this gives the first semantics for handling time and verifying temporal behaviors.

Chapter 6 presents a general model for composing temporal behaviors and systems. It gives the semantics of temporal composition by a new model, Time Stream PN, for composing autonomous (temporal) flows. It emphasizes their interests and applications for systems having independent temporal constraints, which sometimes interact.

Chapters 7 and 8 again consider PNs, i.e. non-temporal PN models, but define an abbreviation of a PN by a general model, which becomes able to represent, in a very compact way, a given set of similar parallel behaviors. The problems associated with this abbreviation are, on the one hand, to define a compact formalism and, on the other hand, to propose new validation techniques to handle this model, i.e. to avoid the obvious solution that consists of unfolding it into a very large PN.

Chapter 7 presents the main PN abbreviations, while concentrating on Colored PNs, which is the most frequently used model.

Chapter 8 gives one well-defined version of this formalism, Well-formed Colored PNs, which allows the development of efficient analysis techniques.

Chapters 9, 10 and 11 introduce distributions, which take into account probabilistic properties of systems. They introduce stochastic PNs, or SPNs, and define their semantics in terms of stochastic processes, and, for some classes of models, their relationships with Markov chains. The principal methods of analyzing SPNs are then presented. Chapter 9 introduces stochastic PNs.

Chapter 10 introduces well-formed SPNs by combining the formalisms presented in Chapter 7 (Well-formed Colored PNs) and Chapter 9. Modeling a multiprocessor architecture illustrates the expressivity of this formalism and its interest for performance evaluation. Chapter 11 develops a tensorial composition of classical and well-formed SPNs, showing that such a compositional approach reduces the complexity of the corresponding validation.

Part 2

The second part of this volume presents important advanced analysis techniques and finally gives some significant and illustrative case studies.

Chapters 12 and 13 address checking and verifying non-temporal behaviors. They present the main approaches that are based on building and manipulating the (system) accessibility or reachability graph, i.e. the graph representing all possible behaviors of the model. Checking these properties, by algorithms applied to the accessibility graph, suffers from the problems of combinatorial explosion. The general problems to be solved to control such an increase in the number of states, as well as general solutions, are then given. Three specific techniques, based respectively on the unfolding of the colored PNs, on symmetries, and on partial orders, are then presented.

Chapters 14 and 15 focus on the temporal validation of behaviors. Chapter 14 analyzes the relationships existing between symmetry and temporal logic for the verification of properties that depend on the specificities of the system. Chapter 15 introduces a parallel–serial hierarchy of temporal behaviors. This hierarchy simplifies the description of complex systems and is very well adapted for modeling complex multimedia and hypermedia objects, documents, and systems.

Chapter 16 presents how to use the main relationships that exist between linear logic and Petri nets for specification and validation. Logical reasoning is constructed based on the behavior of PNs that does not need to produce the reachability graph. The interest of linear logic is illustrated by showing in particular how to handle symbolic temporal intervals (minimum, maximum).

Chapters 17 and 18 present two important case studies that are illustrative while being manageable and easily understandable. Chapter 17 is devoted to the modeling and design of a multilayered, multimedia architecture that is able to guarantee temporal properties at the application level. Chapter 18 presents the application of PN-based models to performance evaluation in the field of computer-integrated manufacturing systems.

Finally, a conclusion summarizes the contents of this volume.

Part 1

Fundamental Models

Chapter 1

Basic Semantics1

1.1. Automata or state machines

1.1.1. Automata and state machine models

The first models for numerical systems led to the definition of automata, or state machines. Automata or state machines are based on three fundamental assumptions, often implicitly given.

The first two assumptions are as follows:

There exist, for the considered systems, a concept of global state, a set of these global states, and an explicit representation of these states (i.e. they can be precisely defined).

There exists a global initial state, and the behavior (operational behavior) of the system starts from this global initial state:

the behavior moves from the initial state by a set of transitions and goes to other global states, one per transition, called “next states”,

this behavior can be fully described by all the transitions that go from each global state to the next, one per transition, also called next states.

Such a transition between two states will take place when a given enabling event occurs during the evolution of the system.

The description of the transition (of the corresponding system behavior) will be represented in the model by an arc starting from a “before the event” state and going to a next “following the arrival of this event” state.

As a consequence, the full behavior of the model will be described by a global graph that represents the way the system operates, and defines all possible global states (represented by circles) and all possible transitions (represented by arcs) that exist between these states.

Note that this (behavioral) model is built step by step, starting from a state called “the initial state”, a well-defined and specific state from which the behavior starts.

The two preceding assumptions are complemented by a very important one needed to construct the graph, the indivisibility of the transition between two states:

when one event occurs in a given state and triggers a transition between two states, the transition has to be completed before another trigerring event can occur.

This means there is no state between the present state and the next state, as the system leaves the present state and reaches the next state indivisibly (the state reached when this transition occurs).

In general, automata and sequential machines are related to their environment by inputs and outputs: the evolution of the model depends on the values of the inputs. In particular, the transitions between two states depend on the values of the inputs. In each state, a value of the inputs can trigger or enable the execution of one transition (each input being able to trigger or enable one transition). The outputs are produced either in a state or during a transition (i.e. a pair state/input or a pair arc/output).

As soon as one input in a given state enables a transition, the transition is executed: its execution starts from the present state and leads to the next state, and produces new values for the outputs.

In this model, the assumption of indivisibility implies:

first, that the transition is executed when the significative input of the automata enables the transition; and

second, that the next state has to be reached before a new input enables a transition in the next state (of the automata or state machine).

Indivisibility with inputs and outputs means that a transition and its outputs (the actions coming from this transition) must be completed before reaching the next state, i.e. before the arrival of an event that can enable one of the transitions starting from the next state (the state newly reached).

Thus, a global behavior of the model can be defined by considering, one after the other, the set of the inputs, transitions, and outputs that define the system execution.

Furthermore, note that the assumption of indivisibility implies that when complex actions (e.g. related to many outputs or to computations) are associated with a transition, these actions must be completed before reaching, and thus defining, the next state.