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.
- This system has a problem: Please run this example in the LTSA tool. You will see that the Safetycheck finds a problem.
- Please explain in a few words the nature of the problem and why this problem exists in this example specification.
- Also, propose a solution to this problem and check with the LTSA tool. Give a short explanation.
- 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.
- Please provide on paper the definition of your model (by copying from the UPPAAL tool) and a short explanation.
Q2 - Things you can prove about your model of Q1(2): Please provide the following information:
- Write down in English a list of assertions about the behavior of your model that you expect to be valid or not valid.
- Try to formulate each assertion in temporal logic accepted by UPPAAL: Give the formal definition of this assertion as accepted by UPPAAL or state that you could not find an acceptable formal definition of it (and explain why, if possible)
- If the assertion was accepted by UPPAAL, what was the verdict of UPPAAL ? (true or false). Explain why this verdict is correct. If the assertion is not accepted by UPPAAL, explain why you think your assertion is valid or not valid.
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.
- 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).
- Question: Please compare the LTSA reachability graph with the one given in the paper. How can the number 21 of reached states by LTSA be explained ? - Is the result of LTSA consistent with what is in the paper ?
- 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).
- How could you explain that the number of states is so much bigger in this case ?