1. (24 points) For each of the following properties: label as either safety or liveness. Give an accompanying counter-example to the property. If the property is a safety property, further indicate if it is a regular safety property, and if regular, give the NFA to verify it.

• The number of items in a buffer may not exceed $n$
• If a process reaches a location $l_i$ just before a critical section, it should not be blocked forever
• Clients may not retain resources forever
• It is always cloudy immediately before it rains
• The transition from $\neg p$ to $p$ will happen at most once
• There are infinitely many transitions from $\neg p$ to $p$ (and vice versa)
• The lights of a traffic signal light in the following periodic sequence: red, yellow, green, red, yellow, green,… and only one light is on at any given time, starting with red.
• If $q$ holds in a state $s_i$ and $r$ holds in some subsequent state $(s_j , j > i)$ then $p$ must not hold in any state $s_k$ in between $s_i$ and $s_j$ ($i < k < j$ , where $j$ is the first such subsequent state)

2. (20 points) This problem is Exercise 5.5 in Principles of Model Checking (page 321 of the PDF document). Consider an elevator system that services N > 0 floors numbered 0 through N-1. There is an elevator door at each floor with a call-button and an indicator light that signals whether or not the elevator has been called. The system must have the following properties:

• Any door on any floor is never open when the elevator is not present
• A requested floor will be served eventually
• The elevator repeatedly returns to floor 0
• When the top floor is requested, the elevator serves it immediately and does not stop on any floor on the way up

Write a PROMELA verification model for the elevator. Identify which properties are safety properties. For the safety properties, verifying them with assertions or with a never claim if the bad prefixes can be described by a regular language.

3. (30 points) This problem is Exercise 5.25 in Principles of Model Checking (page 327 of the PDF document). Consider an arbitrary, but finite, number of identical processes, that execute in parallel. Each process consists of a noncritical part and a critical part, usually called the critical section. In this exercise we are concerned with the verification of a mutual exclusion protocol, that is, a protocol that should ensure that at any moment of time at most one process (among the N processes in our configuration) is in its critical section. In this exercise we are concerned with Szymanski’s protocol. Assume there are N processes for some fixed N > 0. There is a global variable, referred to as flag, which is an array of length N, such that flag[i] is a value between 0 and 4 (for $0 \le i < N$). The idea is that flag[i] indicates the status of process i. The protocol executed by process i looks as follows:

l0: loop forever do begin
l1: Noncritical section 
l2: flag[i] := 1;
l3: wait until (flag[0] < 3 and flag[1] < 3 and . . . and flag[N-1] < 3) 
l4: flag[i] := 3;
l5: if (flag[0]=1 or flag[1]=1 or ... or flag[N-1]=1)
     then begin
        l6: flag[i] := 2;
        l7: wait until (flag[0] = 4 or flag[1] = 4 or ... or flag[N-1] = 4) 
     end
l8: flag[i] := 4;
l9: wait until (flag[0] < 2 and flag[1] < 2 and ... and flag[i-1] < 2)
l10: Critical section
l11: wait until (flag[i+1] ∈ {0,1,4}) and ... and (flag[N-1] ∈ {0,1,4}) 
l12: flag[i] := 0;
end.

Before doing any of the exercises listed below, try first to informally understand what the protocol is doing and why it could be correct in the sense that mutual exclusion is ensured. If you are convinced of the fact that the correctness of this protocol is not easy to see (otherwise please inform me) then start with the following questions.

1. Model Szymanski’s protocol in Promela. Assume that all tests on the global variable flag (such as the one in statement l3) are atomic. Look carefully at the indices of the variable flag used in the tests. Make the protocol description modular such that the number of processes can be changed easily.
2. Check for several values of N (N >= 2) that the protocol indeed ensures mutual exclusion. Report your results for N equal to 4.
3. The code that a process has to go through before reaching the critical section can be divided into several segments. We refer to statement l4 as the doorway, to segments l5, l6, and l7, as the waiting room and to segments l8 through l12 (which contains the critical section) as the inner sanctum. You are requested to check the following basic claims using assertions. Give for each case the changes to your original Promela specification for Szymanski’s protocol and present the verification results. In case of negative results, simulate the counterexample by means of guided simulation.
   1. Whenever some process is in the inner sanctum, the doorway is locked, that is, no process is at location l4.
   2. If a process i is at l10, l11 or l12, then it has the least index of all the processes in the waiting room and the inner sanctum.
   3. If some process is at l12, then all processes in the waiting room and in the inner sanctum must have flag value 4.

4. (30 points) This problem is Exercise 5.26 in Principles of Model Checking (page 328 of the PDF document). We assume N processes in a ring topology, connected by unbounded queues. A process can only send messages in a clockwise manner. Initially, each process has a unique identifier ident (which is assumed to be a natural number). A process can be either active or relaying. Initially a process is active. In Peterson’s leader election algorithm (1982) each process in the ring carries out the following task:

active:
d := ident; 
do forever 
begin
  /* start phase */
  send(d);
  receive(e);
  if e = ident then announce elected; 
  if d > e then send(d) else send(e); 
  receive(f );
  if f = ident then announce elected;
  if e >= max(d,f) then d := e else goto relay; 
end
 
relay:
do forever 
begin
  receive(d);
  if d = ident then announce elected;
  send(d)
end

Model Peterson’s leader election protocol in Promela (avoiding invalid end states) and verify any of the following properties that are regular safety properties:

1. There is always at most one leader.
2. Eventually always a leader will be elected.
3. The elected leader will be the process with the highest number.

5. (20 points) Do Exercise 4.5 in Principles of Model Checking (page 236 of the PDF document). The question asks to compute the intersection of an Automaton with a labeled transition system. Show the automaton for the resulting intersection. Is the language empty?