CSI-5174 - Assignment 3: Play with the Spin tool : Study the ABP

Given: Oct. 14 - - Due: Oct. 21 - revised due date: Nov. 10 (Tuesday, for the class at 14:00 in room LMX-342)

The ABP was already the topic of Question 3 in Assignment 2. Here is a tutorial of the Spin tool. Your tasks are the following:

  1. Prepare a system model of the ABP using a variable for representing the current valid bit, similar as shown on slide 41 of the Spin tutorial. Note that the system on slide 41 has no component representing the communication medium - therefore each sent message is received as such - there is never a transmission error. You should add a transmission component similar as in my paper on the ABP. You may also add components representing the sending and receiving users - this may simplify the formulation of correct data reception - see below. Explain the structure of your ABP system and mention any difficulty you had with using the Promela functions to realize your system description.
  2. Use Spin to verify that there are no deadlocks. Play with different queue sizes, including zero, 1 and 2 and observe the number of states reached in the reachability analysis performed by Spin. Also study the topic of ATOMIC (see tutorial slide 47 and following) and possibly introduce some atomic keywords in your Promela code and check what impact this has on the number of reachable "states". Assume that there is no message loss and no timeout. Explain your findings - does it make sense ?
  3. Compare the number of states in the reachability graphs obtained under point (2) witt (a) those in my paper, and (b) those obtained with Uppaal in Question 3 of Assignment 2. Explain your findings, and try to explain any differences that may be observed.
  4. Introduce the posssibility of message loss and a timeout in the Sender component. Redo points (2) and (3) above.
  5. Study the Spin tutorial concerning the expression of Properties (slide 60 and following). Introduce some statement(s) that state the property that the data sent by the sending user is correctly (and in sequence) received by the receiving user. Use Spin to verify this property. Explain why you selected the given formulation of correct delivery, and any difficulties in uising the Promela functions to express what you had in mind.