代写代考 PN01 I: Foundations

Modelling Complex Software Systems
Lecture PN01 I: Foundations
Artem Polyvyanyy,

Copyright By PowCoder代写 加微信 powcoder

Semester 1, 2022

Introduction to Petri nets
Elementary net systems

How it began
 It is generally not possible to predict how much space calculations of a recursive function will consume
 The data processing system that performs recursive calculations should be expandable if the available resources are insufficient for completing a calculation
 Expanding a system is more efficient than starting over with a larger system
 How can a system architecture that can be expanded indefinitely be described?
 Every expansion of such an expandable architecture enlarges system in space
 Hence, such an indefinitely expandable system must be characterized by:
 No central components
 No central, synchronizing clock

How it began
 In his dissertation “Kommunikation mit Automaten”[1] (Communication with Automata), Petri shows how to construct an indefinitely expandable asynchronous system architecture
 Petri’s systems are composed of locally confined components communicating via local interfaces by performing actions with local causes and effects
 Only later when Petri started to use a graphical representation of his systems, the term “Petri net” was coined
 So, Petri’s dissertation does not contain a single Petri net!
 Petri nets is one of the most popular concepts in computer science
 Legends say that Petri invented Petri nets in August 1939 at the age of 13 for the purpose of describing chemical processes

Components of a net structure
A Petri net is a directed graph with two types of nodes: places and transitions.[2]
 A place p is a passive system component
 Graphically represented as a circle or ellipse
 A place has discrete states and can store things
Transitions
 A transition t is an active system component
 Graphically represented as a square or rectangle
 A transition consumes, produces, or transfers things
 An arc is not a system component but a logical relation between system components
 Graphically represented as an arrow
 An arc relates a place to a transition or a transition to
a place; hence, a Petri net is a directed bipartite graph

Net structures
Sets of places, transitions, and arcs of a Petri net are customary denoted by , , and , respectively. As arcs model relation between places and transitions,  is definedasarelation⊆ × ∪ × .Then,
 = (,,)
is a net structure. Places and transitions are the elements of , and  is the flow
relation of .
Figure: A net structure (,,) with  = A,B,C,D,E ,  = a,b,c,d , and = A,a, a,B, B,b, b,A, B,c, c,A, C,c, c,D, c,E, E,d .

A marking encodes a state of a system and is an arrangement of tokens across places of a net structure.
 A token can represent a thing from the real-world that can be consumed, produced, or transferred by a transition
 A token can indicate a condition that is satisfied for an occurrence of a transition
 Tokens are placed inside circles and ellipses that depict places and are graphically represented as black dots
 A symbolic token can be used instead of a black dot to refer to a concrete thing (e.g.,,, and)
Elementary net systems only use black dot tokens (i.e., tokens abstract from the nature of things they represent).

Introduction to Petri nets
Elementary net systems

Elementary net systems
An (elementary) net system  is a pair , , where  = ,, is
a net structure with finite disjoint sets of places and transitions (i.e.,  ∩  = ∅) and  ∶  → N is an initial marking.[2]
 N is the set of all natural numbers including zero (i.e., non-negative integers)  Each place  ∈  holds   tokens
 Net system  merely describes current state of control flow and availability of
 = A,1, B,0, C,2, D,0, E,0 or =ACC. 
Figure: An abstract model of a cookie vending machine in the initial marking

Pre-set and post-set of an element
Given a net structure , ,  , the pre-set $ and the post-set $ of an element $ ∈  ∪  are defined as follows:
$=%&’ (∈∪ (,$ ∈ and $=%&’ (∈∪$,(∈.
Figure:(a)Pre-setz= A,D,E,F and(b)post-setz= A,B,C,D oftransitionz.

The transition enablement rule
Given a net system , , where  = ,, , marking  enables transition , ∈  if every place in the pre-set of , contains at least one token (i.e., ∀  ∈ ⦁,: () ≥ 1).
Figure: A net system and its only enabled transition a.

The step rule
An enabled in marking  transition , can occur. An occurrence of , results in a step A , where marking ′ is the next state of the system obtained from  by first
destroying one token in every place in the pre-set of , and then creating one fresh
token in every place in the post-set of ,.
The number of tokens at place  ∈  in marking ′ is defined as follows:
 −1 ∈,∧∉, 2  =%&’3 +1 ∈,∧∉,
  otherwise.
Figure: An example step ABBDDEFFF 1 ABBBCDDFF induced by occurrence of transition z. 12 / 19

An abstract model of a cookie vending machine
We will use WoPeD to explore the behaviour of the presented abstract model of a cookie vending machine.
You can download WoPeD from https://woped.dhbw-karlsruhe.de/.

An abstract model of a cookie vending machine

An abstract model of a cookie vending machine

Hot and cold transitions
So far, we have assumed that an enabled transition will either eventually become disabled or occur. This is indeed true for transitions “return coin (b)” and “c”, which
are internal to the system. For example, a coin in the coin slot will eventually be transferred to the coin bank or returned. We refer to such transitions as hot transitions.
However, in the real-world, transitions “insert coin (a)” and “take cookie (d)” are triggered by a customer (an external system), and it is not guaranteed whether they will ever occur. We refer to such transitions as cold transitions and denote them with B.
Cold transitions are rare and are often found at the interface to the environment.[2]
Figure: Cold transitions of the cookie vending machine.

Petri nets in Software Engineering
 Petri nets can be used to build, analyse, and simulate abstract models of software  A net system can represent the control flow of a distributed algorithm or describe
a simple data structure
Figure: A simple non-sequential program for adding two natural numbers.[3]

Petri nets provide a natural formalism for describing distributed systems (e.g., distributed databases and asynchronous communication protocols)
A Petri net describes a system composed of components that perform actions with local causes and effects
A net structure describes passive and active components of a system and logical relations between the components as a bipartite directed graph
A net system is a net structure and a marking that represents the current state of the system
Several transitions of a net system can be enabled for occurrence simultaneously, but only one enabled transition gets chosen non- deterministically to occur
An occurrence of a transition leads the system to a fresh state that gets computed based on the current state using the deterministic step rule
There is a rich body of knowledge on methods for verifying formal properties of systems described as Petri nets (e.g., reachability, boundedness, liveness)

Further Reading
1. mit Automaten. Institut für , Bonn, IIM Report No. 2 (1962) http://edoc.sub.uni-hamburg.de/informatik/volltexte/2011/160/
2. : Understanding – Modeling Techniques, Analysis Methods, Case Studies. Springer 2013, ISBN 978-3-642-33277-7 https://doi.org/10.1007/978-3-642-33278-4
3. : : An Introduction. EATCS Monographs on Theoretical Computer Science 4, Springer 1985, ISBN 3-540-13723-8 https://doi.org/10.1007/978-3-642-69968-9
4. : – Properties, Analysis and Applications. Proceedings of the IEEE, 77 (4), pp. 541-580 (1989) http://dx.doi.org/10.1109/5.24143
5. Jörg Desel, ́s: “What Is a ?” Informal Answers for the Informed Reader. Springer 2001, LNCS 2128, pp. 1-25
https://doi.org/10.1007/3-540-45541-8_1
6. and : Petri and “ .” Advances in Computer Science and Engineering. Fundamental Concepts in Computer Science, vol. 3, pp. 129-139 (2009) https://www2.informatik.uni-hamburg.de/TGI/PetriNets/history/CAPetriAndPetriNets.pdf
7. The World community: https://www2.informatik.uni-hamburg.de/TGI/PetriNets/

程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com