CSI-5174 - Assignment 2: Play with input-output models and UPPAAL

Given: Oct. 7- - Due: Oct. 14

Preliminary: Down-load the UPPAAL tool and study the Train-Gate example given in the Demo folder, including the temporal logic assertions mentioned under the Verifier option.

Q1 - Building a model: Look at the CommProtocol-Simple - modified example given for the LTSA tool.

  1. This system has a problem: Please run this example in the LTSA tool. You will see that the Safetycheck finds a problem.
  2. Prepare in UPPAAL a similar model, including also two user components: Sender and Receivert. Extend the LTSA model in such a way that your model includes the transmission of data (an integer value) in each send and receive operation. It is your design choice to decide how the Sender determines the next data value to be sent, or whether that remains non-determined.

Q2 - Things you can prove about your model of Q1(2): Please provide the following information:

Q3 - Discussion of verification of the alternating bit protocol (ABP)

The verification of the ABP is described in my paper, in particular see Figure 5.

  1. A model of the ABP (without message loss) for anlysis with LTSA is given here. LTSA shows 21 states in the reachability graph (please have a look using the Draw function of the tool).
  2. A model of the ABP (with message loss and a time, as in the paper) for anlysis with LTSA is given here. LTSA shows 109 states in the reachability graph (the Draw function of the tool does not support this big graphs).