SOFT40171 - Design and Development of Secure Systems - Week 3 - Petri Nets Features PDF

SOFT40171 – Design and Development of Secure Systems Week 3 – Petri Nets Features Dr Alexandros Konios 18/02/2025 Agenda  Recall core definitions of Petri Nets  Use Petri Nets to model system features  Modelling Data Flow structures  Net properties in Petri Nets...

SOFT40171 – Design and Development of Secure Systems Week 3 – Petri Nets Features Dr Alexandros Konios 18/02/2025 Agenda  Recall core definitions of Petri Nets  Use Petri Nets to model system features  Modelling Data Flow structures  Net properties in Petri Nets Week 3 –Petri Nets Features Learning Objectives Upon completion of this session, you should be able to:  Recall Petri Nets definitions  Explain the system features modelled using Petri Nets  Apply Petri Nets data flow structures  Understand net properties in Petri Nets Week 3 –Petri Nets Features Petri Nets – Recall Definitions 18/02/2025 Petri Nets – Formal Definition A Petri net is a tuple PN = (P, T, F, M0, 𝓁) where:  P is a finite set of places  T is a finite set of transitions  F ⊆ (P×T)∪(T×P) is the flow relation (we draw an arc from x to y whenever (x,y)∈F)  M0: P → {0, 1, 2,...} is the initial marking  𝓁 : T → 𝛴 is a labelling of transitions using some alphabet 𝛴 of symbols (optional) Week 3 –Petri Nets Features Firing Sequence and Reachable Marking Notation: M[t〉M′ means that transition t is enabled at marking M, and firing it leads to marking M′ Firing Sequence and Reachable Marking Starting from the initial marking M0, we may fire a sequence of transitions t1t2…tn if there are markings M1,M2, …, Mn such that M0[t1〉 M1[t2〉 M2 … Mn-1[tn〉 Mn Then fs = 𝓁(t1) 𝓁(t2)… 𝓁(tn) is a firing sequence, and Mn is a reachable marking Firing sequences represent what an observer of the system would see (i.e., system functioning), and reachable markings are the (global) states the system can find itself in. Week 3 –Petri Nets Features Reachability Graph A Reachability Graph (RG) is defined as a labelled directed graph RG(PN) = (V, Arcs, v0) where:  V is the set of nodes, i.e., all reachable markings  Arcs is the set of labelled arcs: there is an arc labelled a from M to M′ iff for some transition t, M[t〉M′ and 𝓁(t)=a  v0 is the initial node: initial marking M0 Reachability Graph represents all the reachable markings and firing sequences of a PN Theorem: fs is a firing sequence of PN iff there is a directed path from the initial node (i.e., v0) of RG(PN) such that fs is the sequence of arc labels encountered along this path. Week 3 –Petri Nets Features Petri Nets – Modelling System Features 18/02/2025 Petri Nets – Sequential Execution Sequential execution can capture the precedence constraints related to the actions that take place during a system’s operation. Week 3 –Petri Nets Features Petri Nets – Synchronisation Modelling with Petri Nets enables the representation of resources synchronisation for the tasks or actions involved in a system’s behaviour. Week 3 –Petri Nets Features Petri Nets – Conflict Petri Nets can also model choices among available system’s tasks or user’s actions. Week 3 –Petri Nets Features Petri Nets – Mutual Exclusion Petri Nets can successfully model the sharing of resources used within a system. Note: Performing actions (executing transitions) that share resources results in disabling the execution (firing) of one (or more) of the available actions (transitions). Week 3 –Petri Nets Features Petri Nets – Fork Fork in Petri Nets multiples the resources (tokens) to represent resources required for system’s operation. Week 3 –Petri Nets Features Petri Nets – Join Join in Petri Nets reduces the resources (tokens) to represent resources joint together for making another resource required for system’s operation. Week 3 –Petri Nets Features Petri Nets – Modelling Data Flow Structures 18/02/2025 IF - Else Conditional data flow structures (i.e., If – Else) can be constructing using Petri Nets. 1 if C 2 then S1 3 else S2 4 end if Week 3 –Petri Nets Features Case (Switch) Case/Switch statements can be modelled using Petri Nets. 1 Case A Do S1 2 Case B Do S2 3 Case C Do S3 4 Case D Do S4 Week 3 –Petri Nets Features While Loop While loops can be represented using Petri Nets. 1 while C loop 2 S1 3 end loop Week 3 –Petri Nets Features For Loop Also, For loops can be modelled via Petri Nets. 1 For x < 3 Do 2 S1 3 x ++ 3 End loop Week 3 –Petri Nets Features Petri Nets – Net Properties 18/02/2025 Reachability and Boundedness Properties Reachability:  The reachability set R(N,m) of a net N is the set of all markings m reachable from initial marking m0. Boundedness:  A net N with initial marking m0 is safe iff all places always hold at most 1 token.  A marked net is k-bounded iff places hold no more than k tokens.  A marked net is conservative if the number of tokens is constant. Week 3 –Petri Nets Features Liveness and Deadlock Liveness:  A Petri net (N,M0) is said to be live (or equivalently M0 is said to be a live marking of N) if, no matter what marking has been reached from M0, it is possible to ultimately fire any transition of the net by progressing through some further firing sequence. Deadlock:  A deadlock in a transition appears when that transition can never fire or be executed. Note:  A live Petri net guarantees deadlock-free operation, no matter what firing sequence is chosen. Week 3 –Petri Nets Features Summary The most important points of this session are summarised below:  Petri Nets can capture different system features effectively.  Petri Nets can represent logical and programming structures.  Net properties are well-defined in Petri Nets, providing useful information about a system’s behaviour. Week 3 – Petri Nets Features Any Questions?