Assignment 2

Due
on June 19, 2006- 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?

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.

- Read chapter 11 (pp. 109-123) in B. Berard et al. "Systems and Software verification".

- 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.
- 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.
- 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.

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.

- 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.
- Prove that definition 1 and
definition 3 of the free-choice nets
are equivalent (see the definitions at the slides).

- 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. - 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?