Software Engineering Using Formal Methods


Exercises Week 2 - Introducing PROMELA and basic concurrency problems.

These exercises are built on Lectures 2, 3 and 4 of the course.


Recommended

1-4.


Solutions can be found here


Slides about the introduction to the SPIN Web-interface can be found here


Part I. Some features in PROMELA


1. Nondeterminism

The following piece of code shows nondeterministic nature of PROMELA if.
active proctype NONDET() { 
  if 
    :: true -> printf("1\n")
    :: true ; printf("2\n")
    :: printf("3\n")
  fi
}

Launch in web-interface

Run a few random simulations. What do you notice ?

Note that nondeterministic choice of a guard is not limited to if statement only. To observe this let us introduce a minimal change to the code above and replace if with do (and fi with od respectively). Run a random simulation of the modified model.

Else or True?

Let us examine the following two PROMELA programs.

active proctype TRUE() { 
  if
    :: false -> printf("1\n")
    :: true  -> printf("2\n")
  fi
}
active proctype ELSE() {  
  if
    :: false -> printf("1\n")
    :: else  -> printf("2\n")
  fi
}

Launch in web-interface

By running these two programs we observe that both of them always produce 2 as their output. Based on this example, can we generalize that else can be replaced by true in our PROMELA programs? Can you find other examples that support this claim? How do you back up your answer?


2. Arrays

As a running example of this section we write a PROMELA model for summing up an array of integers. As a starting point here is a program that declares and nondeterministically initializes an integer array.

#define N 10

active proctype ARRAY() {
  int a[N]; 
  int s = 0;
  int sum = 0;
  
  /* use Nondeterminism to fill the array with some values */
  do
    :: (s >= N) -> break
    :: else     -> if 
		     ::  a[s] = 0
		     ::  a[s] = 1
		     ::  a[s] = 2
		     ::  a[s] = 3
		     ::  a[s] = 4
		     ::  a[s] = 5
		   fi;
		   s++
  od;
  
  printf("The sum is: %d\n", sum)
}

Launch in web-interface

Running this program always produces 0 as an output. Complete the example by adding a loop that sums up the array elements. Use one of the variants of a loop statement that you have experimented with earlier in this exercise. Once you are done with that rerun the resulting program. Note that due to nondeterminism in the initialization you will obtain different outputs with every run. One way to force determinism in this example is to remove (or comment out) lines corresponding to guards generating values 0 to 4. PROMELA uses C-like /* ... */ comments. If you try this out and rerun the program several times you should get 50 produced as the output in all runs.


Part II. Modelling concurrency with shared variables and verification of concurrent programs


3

Going back to the equivalence of True and Else from exercise 1, verify formally that the processes TRUE and ELSE don't always output the same thing in the general case. For this purpose you can use ghost variables and you can start the process from init, wait until both are finished using the "joining" trick from the lectures and thereafter make the assertion. Note that you need to initialize b, before running the processes!

bool b;

proctype TRUE() { 
  if
    :: b -> printf("1\n")
    :: true  -> printf("2\n")
  fi
}

proctype ELSE() {  
  if
    :: b -> printf("1\n")
    :: else  -> printf("2\n")
  fi
}

Launch in web-interface


4

Define a process p() that increases a global variable b like this:

byte b = 0;

proctype p() {
b ++
}

Change process p as follows:

proctype p() {
byte tmp = b;
tmp ++;
b = tmp
}
For both versions of p(), proceed in the following manner: start two instances of p, wait until both are finished and thereafter assert that (b == 2).
  1. Will the assertion be true ?
  2. If not, what other values can b have ?
  3. Generalize the program by starting N instances of p, 5 for example. What values can b take in this case ? Verify your hypothesis with an appropriate assertion.
  4. Can b be 2 in this case ? Use spin to find a scenario when this happens.
  5. Try to fix the code so that b will always be N in the end.

5

Model an office where two computer systems are hooked up to a single printer. Establish mutual exclusion between the two computer systems using a global variable and atomic "test & set" operations. Verify that it is never the case that both systems print at the same time.


6

Model the following scenario: 12 people want to book a ping-pong table. The table can only be used by 2 people at a time - not more, not less. Of course, in the beginning it will be free, until the first 2 players have access to it. However, no one can play alone, until they find a partner.

Each player is a process. They only try to book the table and don't communicate with each other.

Hint: use shared variables to model the table and the waiting list you keep. This can be a variable marking the pid of the player who is waiting for a partner.

Extra: In the version suggested above, all other players who make additional requests will be denied and their requests are lost, because we only keep the first successful request. You can modify that with a waiting list that is an array. What length should it have and why ?

After writing the code, think about properties that express the correct behaviour of your system and check them in spin.

References

  • Spin reference card (PDF)

Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools Last Modified: 10 Sep 2015