Assignment 2
Due on June 19, 2006

#### May 1-15

1. Consider the following problem:
Six soldiers who are heavily injured, try to flee to their home land.  The enemy is chasing them and in the middle of the night they arrive at a bridge that spans a river which is the border between the two countries at war.  The bridge has been damaged and can only carry two soldiers at a time.  Furthermore, several land-mines have been placed on the bridge and a torch is needed to sidestep all the mines.  The enemy is on their trail, so the soldiers know that they have only 2 hours to cross the bridge.  The soldiers only have a single torch and they are not equally injured.  The following table lists the crossing times (one-way!) for each of the soldiers:

soldier S0   5 minutes
soldier S1  10 minutes
soldier S2  20 minutes
soldier S3  25 minutes
soldier S4  30 minutes
soldier S5  35 minutes

Does a schedule exist which gets all six soldiers to the safe side within 120 minutes?
(Ruys & Brinksma 1998)

In essence, this is a scheduling/planning problem, and we can take advantage of the fact that a model-checker explores all possible orders of interleavings. Thus, we can easily have the model-checker construct all the different orderings for moving soldiers across the bridge.
We would like to get SPIN to generate a trace for us that illustrates a schedule where the soldiers can get from the unsafe to the safe side in 120 minutes or less. SPIN generates counter-example or property-violation traces.  Therefore, we need to ask SPIN to try to prove that a schedule does not exist.  If it finds a counterexample, it will illustrate a schedule that is a solution to the soldiers problem.
Using Linear Temporal Logic, we can formalize the desired property directly. One can also get SPIN to generate an appropriate trace using an assertion.
You have to build a Promela model to solve this problem and generate a trace illustrating some "good" schedule.

1. Consider two transition systems:

Is that true that
1. the systems are trace equivalent?
2. T1 <= T2?
3. T2 <= T1?
4. T1 is bisimilar to T2?
Argue why yes or why not.

#### May 22-29

1. Read chapter 11 (pp. 109-123) in B. Berard et al. "Systems and Software verification".
1. Abstract the timer at the sender side in your Promela model of PAR, check how the abstract version of the protocol works for several timer settings.
2. Use the model you built for problem 4 and redefine the environment by using data independence; formulate the correctness property first in the textual form, then formalise it; check the property with Spin for several "good" timer settings. Interpret the results in a natural language.
3. In this exercise we consider a list abstraction that can be used for the verification of protocols that sends packages of messages that we model as lists of natural numbers.We use data independence and abstract natural numbers p1, p2 into e1, e2 respectively, while all the other naturals are non-distinguishable and they are abstracted into an abstract element ne. Now we want to abstract lists of non-repeating naturals numbers. An arbitrary list of naturals is represented by