Petri Nets Features in Secure Systems Design

• SOFT40171 - Design and Development of Secure Systems, delivered in week 3 focuses on Petri Nets Features.

Agenda

• Core Petri Nets definitions are recalled.
• Petri Nets can model system features.
• Data Flow structures can be modelled
• Net properties are explained.

Learning Objectives

• Recall Petri Nets definitions.
• System features are modeled using Petri Nets.
• Petri Nets data flow structures are applied.
• Net properties in Petri Nets are understood.

Petri Nets - Formal Definition

• A Petri net is a tuple PN = (P, T, F, Mo, l).
• P is a finite set of places.
• T is a finite set of transitions.
• F⊆ (PxT)U(TxP) is the flow relation.
• An arc is drawn from x to y whenever (x,y)∈F
• Mo: P → {0, 1, 2, ...} is the initial marking
• l:T → ∑ is a labeling of transitions using some alphabet ∑ of symbols (optional).

Firing Sequence and Reachable Marking

• Notation M[t)M' means transition t is enabled at marking M, and firing it leads to marking M'.
• Starting from the initial marking Mo, a sequence of transitions t₁t₂...tₙ may fire if there are markings M₁,M₂,...,Mₙ such that Mo[t₁) M₁[t₂) M₂... Mₙ₋₁[tₙ) Mₙ
• fₛ = l(t₁) l(t₂)... l(tₙ) is a firing sequence
• Mₙ is a reachable marking
• Firing sequences represent what an observer of the system would see (i.e., system functioning).
• Reachable markings are the (global) states the system can find itself in.

Reachability Graph

• A Reachability Graph (RG) is defined as a labeled directed graph RG(PN) = (V, Arcs, vo).
• V is the set of nodes i.e., all reachable markings.
• Arcs is the set of labeled arcs
• There is an arc labeled a from M to M' if for some transition t, M[t)M' and l(t)=a.
• vo is the initial node: initial marking Mo
• A reachability Graph represents all the reachable markings and firing sequences of a PN.
• A firing sequence fₛ , of PN exists iff there is a directed path from the initial node (i.e., vo) of RG(PN) such that fₛ is the sequence of arc labels encountered along this path.

Petri Nets - Modelling System Features

• Petri Nets provide a way to capture the precedence constraints related to actions during a system's operation using Sequential Execution.
• Petri Nets enables the representation of resources synchronisation for the tasks or actions involved in a system's behaviour, therefore can be used for Synchronisation.
• Petri Nets can model choices among available system's tasks or user's actions withConflict modelling.
• Petri Nets can successfully model the sharing of resources used within a system, with Mutual Exclusion modelling.
• Performing actions (executing transitions) that share resources results in disabling the execution (firing) of one (or more) of the available actions (transitions).
• Fork in Petri Nets multiples the resources (tokens) to represent resources required for system's operation.
• Join in Petri Nets reduces the resources (tokens) to represent resources joint together for making another resource required for system's operation.

Petri Nets - Modelling Data Flow Structures

• Conditional data flow structures (i.e., If – Else) can be constructed using Petri Nets.
• Case/Switch statements can be modeled using Petri Nets.
• While loops can be represented using Petri Nets.
• For loops can be modeled via Petri Nets.

Petri Nets - Net Properties

• Reachability helps determine the set of all markings m' reachable from initial marking mo, notated as R(N,m) for a net N.
• A net N with initial marking mo is considered safe if all places always hold at most 1 token.
• A marked net is k-bounded if places hold no more than k tokens.
• A marked net is conservative if the number of tokens is constant.
• A Petri net (N,Mo) is said to be live (or equivalently Mo is said to be a live marking of N) if, no matter what marking has been reached from Mo, it is possible to ultimately fire any transition of the net by progressing through some further firing sequence.
• A deadlock in a transition appears when that transition can never fire or be executed.
• A live Petri net guarantees deadlock-free operation, no matter what firing sequence is chosen.

Summary

• 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.

This lesson covers Petri Nets, recalling core definitions and explaining how they can model system features. Data flow structures are modeled. It also explains properties of Petri Nets.