Assignment 1

Due on May 4

The parts of the assignment you have to hand in are in this colour.

April 3 - April 10

  1. Read the following two papers:
Write 3 well-reasoned statements for each paper. That could be something you especially liked/unliked, something you believe to be very important in process modelling, etc. (max. 1 page in total). That should not be just citations from the papers.
  1. Read the information about Spin at http://spinroot.com/spin/whatispin.html, http://spinroot.com/spin/Man/Quick.html and http://spinroot.com/spin/Man/Manual.html; 
Download a copy of Spin; downloading and installation instructions: https://www.win.tue.nl/~rp/spin/ (or http://spinroot.com/spin/) ;

Start experimenting with Spin a little (just simulation and checks for deadlocks); follow the instructions from http://spinroot.com/spin/Man/GettingStarted.html ; take (at least) examples 2 and 5 from http://spinroot.com/spin/Man/Exercises.html

Read pages 1-2 in the description of a model of a very simple elevator (elevator.pdf); the model itself is given in elevator.pml.
  1. One of the problems with the elevator example is that the elevator doors can repeatedly open and close without the elevator changing floors. Change the model (i.e., edit the Promela code) so that this cannot happen (so you hand in your Promela model with a short description of what you have changed). (Caution: Do not eliminate any other allowed behaviours! Eliminate only opening and closing immediately followed by another opening and closing.)
  2. Another problem with the original elevator example is that the elevator doors can open and close without a request from a user. Change the original elevator model — not the improved model that you produced for 2.1 — so that this cannot happen: introduce a button process for each door; the button is randomly “pressed”, and the elevator will open and close the doors when it is at a floor if and only if the button for that floor has been pressed. (Caution: This means that you should allow the door to open and close for a second time when the button is re-pressed before the elevator leaves the floor.)

April 10-17

  1. Is there an LTL equivalent of the CTL formula AG EF p ? If “yes”, provide the formula. If “no”, you can just answer “no”, but you get extra credit if you can show there is no such formula (in case you have troubles with CTL, see Chapter 2 of B. Berard et al., Systems and Software Verification. Model Checking Techniques and Tools).
  2. Are CTL formulas AG AX p and AXAG p equivalent? If your answer is “yes”, justify it. If your answer is “no”, provide a counterexample. (in case you have troubles with CTL, see Chapter 2 of B. Berard et al., Systems and Software Verification. Model Checking Techniques and Tools).
  3. Formulate 10 (meaningful) requirements for one of the following processes: (1) booking a plain ticket via www.klm.nl or www.klmairmiles.nl; (2) buying books at www.amazon.com or www.bol.com; (3) payments via Internet Banking. Formalize them in a temporal logic. You may use LTL or CTL. At least 2 of these properties should use fairness. (Caution: Do not forget to formulate the atomic propositions you use in your formulas.)
  4. Use Spin to determine for the model that you constructed in 2.1 whether it satisfied the following property: "there is a trace starting at the start state in which, at some time, the first floor door opens twice without either the second floor door or the third floor door opening in between".
  5. Use Spin to determine for the model that you constructed in 2.2 whether it satisfied the following property: "in every trace starting from the start state, every time the button at the second floor is pressed, the door at the second floor will eventually open".
  6. Read Chapter 2 in J. Desel, J. Esparza, "Free Choice Petri Nets". Make sure that you know what the following notions mean: pre-sets, post-sets, markings, occurrence rule, incidence matrix, Parikh vector, Marking Equation Lemma; Properties: Liveness, deadlocks, boundedness,
    S-invariants and T-invariants    . Give solutions to the following problems:
    1. Construct a transition system describing the behaviour of the Petri net in Figure 2.1 (page 17) from [Desel&Esparza]
    2. Use this transition system and find at least 3 LTL properties that hold on it (and hence on the Petri net as well). At least one of these properties should be with the use of a fairness assumption. Note that atomic propositions should be defined on the markings of the net.

April 17-24

  1. To prepare to the next lecture, read chapter 5, pp. 59-68, from B. Berard et al., Systems and Software Verification. Model Checking Techniques and Tools, © Springer Verlag, 2001. At the lecture, I'll assume that you've read it; thus, it may be difficult to follow it if you did not.

April 24-May 1

  1. Make a Promela model of the Positive Acknowledgment with Retransmission protocol (see the description in the lecture handouts). Investigate which settings for the Sender's timer  guarantee the proper functioning of the protocol (assume that the channels' delays are given). With proper functioning, we mean here that at least the following properties hold:
    1. No deadlock happens (assuming that the environment provides an infinite sequence of signals as input) - remember that having a deadlock in the system is not necessarily equivalent to having a deadlock in the model, since tick-actions will continue to happen also when the system is actually deadlocked. So you need to find a way to formulate the deadlock condition.
    2. No overflow for internal buffers happens (hint: use 'len' - see http://www.spinroot.com/spin/Man/len.html - to formulate your verification property).
    3. Every message sent is eventually delivered (under the fairness assumption on the channel behaviour). - You probably won't be able to verify this property as it is formulated here, since you would need to use some additional techniques that we have not discussed yet. Therefore, formulate a simpler property that would not imply the property of interest, but still, the fact that it holds would give you more confidence that the system works correctly and that the property of interest holds on the system.
    You may extend this list with some other properties and get bonus points if you prove them to be true as well.
    Give examples of ``good'' and ``bad'' timer settings.
    Which inequation characterises ``good settings'' from your point of view? (check it for some boundary cases).

  2. Consider a model in Fig. 5.3 of B. Berard et al. "Systems and Software Verification". Does the following trace represent a possible behaviour of that model?
    • ((far,0),(up,0)) -> ((far,2),(up,2)) -> ((near,0),(lower,0)) -> ((near,1.5),(lower,1.5)) -> ((near,1.5),(down,1.5)) -> ((near,3),(down,3)) -> ((on,0),(down,3)) -> ((on,1.5),(down,4.5)) -> ((far,0),(raise,0)) -> ((far,1.5),(raise,1.5)) -> ((far,1.5),(up,1.5)).  Note that ((on,1.5), (down,4.5)) stands for the state of the system where the train is in state 'on' and its clock Ct equals 1.5, while the gate is in state 'down' and its clock Cb equals 4.5.