Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2009 | Buch

Introduction to Modelling and Validation Kapitel lesen Erstes Kapitel lesen

Coloured Petri Nets

Modelling and Validation of Concurrent Systems

verfasst von: Kurt Jensen, Lars M. Kristensen

Verlag: Springer Berlin Heidelberg

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

Coloured Petri Nets (CPN) is a graphical language for modelling and validating concurrent and distributed systems, and other systems in which concurrency plays a major role. The development of such systems is particularly challenging because of inherent intricacies like possible nondeterminism and the immense number of possible execution sequences.

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. An accompanying website offers additional material such as slides, exercises and project proposals.

Book website: http://www.cs.au.dk/CPnets/cpnbook/

Inhaltsverzeichnis

Frontmatter
Chapter 1. Introduction to Modelling and Validation
System development and engineering is a comprehensive discipline involving a multitude of activities such as requirements engineering, design and specification, implementation, testing, and deployment. An increasing number of system development projects are concerned with concurrent systems. There are numerous examples of this, ranging from large-scale systems, in the areas of telecommunication and applications based on Internet technology, to medium- or small- scale systems, in the area of embedded systems.
Kurt Jensen, Lars M. Kristensen
Chapter 2. Non-hierarchical Coloured Petri Nets
This chapter introduces the concepts of non-hierarchical Coloured Petri Nets. This is done by means of a running example consisting of a set of simple communication protocols. Protocols are used because they are easy to explain and understand, and because they involve concurrency, non-determinism, communication, and synchronisation which are key characteristics of concurrent systems. No preliminary knowledge of protocols is assumed.
Kurt Jensen, Lars M. Kristensen
Chapter 3. CPN ML Programming
This chapter presents the CPN ML programming language for defining colour sets and functions, declaring variables, and writing inscriptions in CPN models. The previous chapter has provided a few simple examples of CPN ML programming. This chapter provides a comprehensive introductory road map to the CPN ML programming language. Many other examples of CPN ML programming will be given in later chapters.
Kurt Jensen, Lars M. Kristensen
Chapter 4. Formal Definition of Non-hierarchical Coloured Petri Nets
This chapter gives a formal definition of the syntax and semantics of the nonhierarchical and untimed parts of the CPN modelling language. The formal definition is a supplement to the informal introduction provided in Chap. 2. Readers who are not interested in the mathematical definition and are content with the informal introduction may decide to skip this chapter. The formal definition of the hierarchical constructs will be given in Chap. 6, and that of the timed constructs will be given in Chap. 11.
Kurt Jensen, Lars M. Kristensen
Chapter 5. Hierarchical Coloured Petri Nets
This chapter shows how a CPN model can be organised as a set of modules, in a way similar to that in which programs are organised into modules. There are several reasons why modules are needed. Firstly, it is impractical to draw a CPN model of a large system as a single net, since it would become very large and inconvenient. Although the net can be printed on a set of separate sheets and glued together, it would be difficult to get an overview and it would be time-consuming to produce a nice layout. Secondly, the human modeller needs abstractions that make it possible to concentrate on only a few details at a time. CPN modules can be seen as black boxes, where modellers, when they desire, can forget about the details within modules. This makes it possible to work at different abstraction levels, and hence we shall also refer to CPN models with modules as hierarchical CPN models. Thirdly, there are often system components that are used repeatedly. It would be inefficient to model these components several times. Instead, a module can be defined once and used repeatedly. In this way there is only one description to read, and one description to modify when changes are necessary.
Kurt Jensen, Lars M. Kristensen
Chapter 6. Formal Definition of Hierarchical Coloured Petri Nets
This chapter formally defines the syntax and semantics of hierarchical CPN models. Readers who are not interested in the mathematical definitions and are content with the informal introduction given in the previous chapter may decide to skip this chapter. The definition of hierarchical CPN models relies on the definition of nonhierarchical CPN models, and we assume that the reader is familiar with the formal definitions provided in Chap. 4.
Kurt Jensen, Lars M. Kristensen
Chapter 7. State Spaces and Behavioural Properties
This chapter introduces the basic state space method of CP-nets and shows how it can be used to investigate the behavioural properties of the protocol described in Chap. 2. The basic idea of state spaces is to calculate all reachable states (markings) and state changes (occurring binding elements) of the CPN model and to represent these in a directed graph where the nodes correspond to the set of reachable markings and the arcs correspond to occurring binding elements. The state space of a CPN model can be computed fully automatically and makes it possible to automatically analyse and verify an abundance of properties concerning the behaviour of the model. Examples of such properties include the minimum and maximum numbers of tokens on a place, the states in which the system may terminate, and the system always being able to reach a certain state.
Kurt Jensen, Lars M. Kristensen
Chapter 8. Advanced State Space Methods
This chapter gives an overview and some concrete examples of state space reduction methods. The main limitation of using state spaces to verify behavioural properties of systems is the state explosion problem [106], i.e., that state spaces of systems may have an astronomical number of reachable states, which means that they are too large to be handled with the available computing power (memory and CPU speed). Methods for alleviating this inherent complexity problem are an active area of research, which has led to the development of a large collection of state space reduction methods. These methods have significantly broadened the class of systems that can be verified, and state spaces can now be used to verify systems of industrial size. Some of these methods [18, 61, 62, 108] have been developed in the context of the CPN modelling language. Other methods (e.g., [55, 87, 104, 110]) have been developed outside the context of the CPN modelling language. Most state space reduction methods are independent of the concrete modelling language used and hence are applicable to a large class of such languages.
Kurt Jensen, Lars M. Kristensen
Chapter 9. Formal Definition of State Spaces and Behavioural Properties
This chapter formally defines state spaces and behavioural properties. Readers who are not interested in the mathematical definitions and are content with the informal introduction given in Chap. 7 may decide to skip this chapter. The definition of state spaces relies on the definitions for non-hierarchical CPN models presented in Chap. 4, and it is assumed that we have a non-hierarchical CPN model CPN = (P,T,A,∑ ,V,C,G,E, I) as defined in Definition 4.2. All definitions given in this chapter can be generalised immediately to hierarchical CPN models by replacing places with place instances and transitions with transition instances.
Kurt Jensen, Lars M. Kristensen
Chapter 10. Timed Coloured Petri Nets
This chapter shows how timing information can be added to CPN models. This makes it possible to evaluate how efficiently a system performs its operations and it also makes it possible to model and validate real-time systems [78], where the correctness of the system relies on the proper timing of the events.With a timed CPN model, performance measures such as maximum queue lengths and mean waiting times can be calculated. Also, we may, for example, verify whether the operation of a real-time system meets required deadlines.
Kurt Jensen, Lars M. Kristensen
Chapter 11. Formal Definition of Timed Coloured Petri Nets
This chapter formally defines the syntax and semantics of timed CPN models. Readers who are not interested in the mathematical definitions and are content with the informal introduction given in the previous chapter may decide to skip this chapter. The definition of timed CPN models relies on the definition of untimed nonhierarchical CPN models, and we assume that the reader is familiar with the formal definitions provided in Chap. 4.
Kurt Jensen, Lars M. Kristensen
Chapter 12. Simulation-based Performance Analysis
This chapter shows how simulation of CPN models can be used to investigate the performance of systems and thereby evaluate their efficiency. Performance is a central issue in the design and configuration of concurrent systems, and performance analysis is conducted to evaluate existing or planned systems, to compare alternative implementations, and to find optimal configurations of systems. The basic idea of simulation-based performance analysis is to conduct a number of lengthy simulations of a CPN model, during which data is collected from the occurring binding elements and the markings reached in order to calculate estimates of performance measures of the system. The typical performance measures include average queue lengths, average delays, and throughput.
Kurt Jensen, Lars M. Kristensen
Chapter 13. Behavioural Visualisation
As illustrated in Chap. 2, a user of CPN Tools observes the execution of a CPN model directly in its graphical representation. Even though the CPN modelling language supports abstraction and a concept of hierarchical modules there can still be an overwhelming amount of detail in a constructed CPN model. Furthermore, observing every single step in a simulation is often too detailed a level of observation for investigating the behaviour of a model, especially for large CPN models. This can be a limitation when, for example, presenting a CPN model to colleagues unfamiliar with the CPN modelling language and discussing the model with them. The basic idea of behavioural visualisation is to augment the CPN model with visualisation graphics that reflect the execution of the model.
Kurt Jensen, Lars M. Kristensen
Chapter 14. Examples of Industrial Applications
This chapter presents a selection of representative projects where CP-nets and their supporting computer tools have been used for system development in an industrial context. These projects have been selected to illustrate the fact that CP-nets can be used in many different phases of system development, ranging from requirements specification to design, validation, and implementation. The CPN models presented were constructed in joint projects between our research group at Aarhus University and industrial partners.
Kurt Jensen, Lars M. Kristensen
Chapter 15. Teaching Coloured Petri Nets
This chapter describes a course on the modelling and validation of concurrent systems based on this textbook which we have been giving at the Department of Computer Science, at Aarhus University. The course uses CP-nets as a formal modelling language for concurrency and exposes students to the benefits and applications of modelling for designing and reasoning about the behaviour of concurrent systems. The course introduces participants to the CPN modelling language, its analysis methods, and its supporting computer tools. It also includes a presentation of industrial projects where CP-nets have been used for the modelling and validation of systems. After the course, the participants will have a detailed knowledge of CP-nets and practical experience in the modelling and validation of concurrent systems.
Kurt Jensen, Lars M. Kristensen
Backmatter
Metadaten
Titel
Coloured Petri Nets
verfasst von
Kurt Jensen
Lars M. Kristensen
Copyright-Jahr
2009
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-00284-7
Print ISBN
978-3-642-00283-0
DOI
https://doi.org/10.1007/b95112