VV: Exercise 1, model checking

Petri Nets

Introduction

In this exercise we will use SPIN to verify properties about Petri Nets, a kind of transition graph commonly used for representing concurrent protocols involving shared resources in many areas in Computer Science such as Concurrent Programming, Software Engineering, Workflow modeling, Simulation, Diagnosis or Business Process Modeling. They can be used, for instance, as an alternative to Activity Diagrams in UML.

Definitions: a Petri Net is a graph formed by two disjoint sets of nodes, T and P, respectively called transitions (represented as thick bars) and places (depicted as circles), and a set of arcs A ⊆ (T x P) ∪ (P x T). This means that arcs can go from a place to a transition or vice versa, but will never connect two places or two transitions directly. Given a transition t, we define its incoming places as In(t) := {p | (p,t) ∈ A} and its outgoing places as Out(t) := {p | (t,p) ∈ A}. A marking M of the net is a function M: P -> Nat assigining a natural number to each place in the net. Graphically, if M(p)>0 this is represented by including a number M(p) of black dots (tokens) inside the circle for place p. If M(p)=0 the circle is left empty. A marking is said to be 0-1 if all the places have one or zero tokens. We say that a transition t ∈ T is enabled in a marking M, when M(p)>0 for all input places p ∈ In(t).

Execution: The Petri Net is executed by defining the valid steps from one marking M to another M'. A valid step, represented as M → M', is such that there exists some enabled transition t ∈ T in M that has been fired in M', that is, we have consumed one token from all input places and produced one token for al output places. Formally, M' satisfies:

• M'(p) = M(p)-1 for all p ∈ In(t) \ Out(t)
  
• M'(q) = M(q)+1 for all q∈ Out(t) \ In(t)
• M'(q) = M(q) for all q∈ Out(t) ∩ In(t)

The execution starts from an initial marking denoted as M₀ and proceeds in consecutive steps M₀ → M₁ → M₂ → ...  As we can see, executions can run forever: they only stop when there are no enabled transitions. In a given step, we may have several enabled transitions so that one is chosen non-deterministically. For some execution examples, see this interactive tutorial from TU Eindhoven.

Goals

1. absence of deadlock: we cannot reach a state in which all processes get blocked waiting for something to happen.
2. safety: check that a given (wrong) configuration is not reachable.
   
3. absence of starvation (fairness): check whether some transition is fired infinitely often.
4. boundedness: check that the number of tokens in a given place is bounded.
   

A simple formalization of this problem in Promela can be:

#define Place byte            // assume at most 255 tokens per place Place p1=1, p2=0, p3=0, p4=0  // place p1 has an initial token #define enabled(x)    x>0 -> x-- #define fire(x)       x++ init {   do   :: enabled(p1) -> fire(p2); A1: printf("A1\n")   :: enabled(p2) -> fire(p3); A2: printf("A2\n")   :: enabled(p3) -> fire(p4); A3: printf("A3\n")   :: enabled(p4) -> fire(p3); A4: printf("A4\n")   :: enabled(p3) -> fire(p2); A5: printf("A5\n")   :: enabled(p2) -> fire(p1); A6: printf("A6\n")   od }

Given the initial marking in the picture above, check the following conditions:

• Safety: check whether we could have tokens at two different floors. Explain the obtained result.
  
• Fairness: check that each floor is visited infinitely often. Explain the obtained result.
• Boundedness: check that each place in the net is always marked with 0 or 1 tokens, but not more.

This Petri net represents two traffic lights 1 and 2 that can alternate the sequence Green - Orange - Red but should not be Green simultaneously. The Petri net uses one place per each color and traffic light: G1, O1, R1, G2, O2, R2. It contains an additional place S to guarantee that only one green light is turned on. Using the initial marking depicted above:

• Formalize the problem in Promela
• Safety: check whether a situation in which both traffic lights are green is not reachable. Explain the obtained result.
  
• Fairness: check whether both traffic lights can reach each color infinitely often. Explain the obtained result.
• Boundedness: check that each place in the net is always marked with 0 or 1 tokens, but not more.
• Use SPIN to check if there exists an initial 0-1 marking that violates the boundedness condition above.
  

Assessment & delivery

The maximum grade for this exercise is 1,3 points. The work can be done by groups of 2 students at most: if so, both student names must be included in all promela files as comments in the first lines. To submit your work:

• Connect to any of the computers: 10.10.5.xxx with xxx from 118 to 126 (excepting 124)
• Copy all your files in the directory /PRACTICAS/GEI/VVS/P1/your_login

The deadline for delivery is Friday,  December 18th,  2015 (23:59).