Asignatura Modelización, Ejercicios

This page contains information about the exercise part of the course Modelización (Grado MI) at the Facultad de Informática, UPM. If your English is not good enough to understand the instructions, please consult me directly (lfredlund@fi.upm.es) for information.

Exercises

• Install Uppaal. Start it to see that the graphical interface works.
• Model the following program P1 in Uppaal. The program is composed of two processes that execute the same code, accessing a shared variable:

  while true do if x>0 then x:=x-1 end

  . The initial value of

  x

  should be

  5

  . The statement should be run "atomically" , that is no other statement can execute after the test (

  x>0

  ) and before the assignment (

  x:=x-1

  ).
• Use the Uppaal simulator to simulate the program P1. Hint: first check that it is syntactically correct.
• Model program P2 in Uppaal. P2 is identical to P1 except the execution of the test (

  x>0

  ) and the assignment (

  x:=x-1

  ) is not atomic, i.e., it must be possible for another statements to execute after the test and before the assignment.
• Simulate program P2 in Uppaal. Notice any differences?
• Use the verification functionality in Uppaal to formulate a number of properties (true or not) regarding your programs P1 and P2. Can you formulate a property that distinguishes P1 and P2? (i.e., a property that is satisfied by P1 but not P2, or vice versa).
• Next, select one of the algorithms/systems below. Model it in Uppaal, experiment with it, and verify that your solution is correct.
  • Hyman's mutual exclusion algorithm (non-timed).
  • Fischer's mutual exclusion algorithm (timed).
  • The train gate example in the Uppaal tutorial, beginning at page 15 (timed).
  • The alternating bit protocol (non-timed). Model a transmitter, a receiver and a channel. To simplify the specification, consider only message loss, not message corruption.
  • Much more interesting: your own example.

Read the Tutorials

The two tutorials (shorter, longer) are recommended reading while doing the exercises. Pay special attention to the syntax of properties (the Help menu item is also helpful).

Download Uppaal

• For Linux and Windows.
• For Mac OS X.

If these do not work, try installing the newer versions (Uppaal 4.1) directly from www.uppaal.org.

Installation instructions

To install Uppaal Java (at least version 6) should be installed first. See the readme.txt file (Windows and Linux) for detailed instructions.