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
•  its abstracted head element,
• an abstract representation of the whole list, which is of the form epsl, e1l, e2l, e1e2l, e2e1l, error, and, furthermore,
• the information whether it is an empty or a one-element list.
Here, error is an abstraction for an "incorrect" list, i.e. a list with duplicated elements (the assumption is that only lists of non-repeating naturals are sent, but one need to assure that no repetition takes place at the receiver side as well); epsl represents correct lists where no e1 and no e2 occur, e1l , e2l are representations of correct lists where only e1 (e2 resp.) occurs; e1e2l, e2e1l represent lists where both e1 and e2 occur, in the corresponding orders.
Example:  list  abp1cdp2 will be abstracted to (ne, e1e2l, long-list); list p1 will be abstracted to (e1, e1l, one-el); list aba will be abstracted to (ne, error, long-list).
Define a data type for abstract lists in Promela and the abstract version of the removing of the head element from the list.

#### May 29 - June 5

1. Prove that the Petri net given in Fig. 5.1 (the upper net), p.90 of [Desel, Esparza] is live and bounded by applying reduction techniques preserving liveness, boundedness and safeness.
2. Prove that definition 1 and definition 3 of the free-choice nets are equivalent (see the definitions at the slides).
3. a) Exercise 4.3 from [Desel,Esparza].
b) Find for every net from Exercise 4.3 the set of all markings M such that (N,M) is live.
4. Consider the following two WF-nets. Find out whether they have redundant or persistent places. Can you make any conclusion about the soundness of these nets based on the presence or absence of redundant and persistent places?