Second Mini Project
Modelling and Verification, Spring 2006
Modelling and Analysis of a Realtime Mutual Exclusion Algorithm
The deadline for delivering this miniproject is Friday, 10 March,
2006 at 20:00. Deliver your solution via the intranet if you are a
student at RU and via email otherwise. (Those of you who deliver by
email should receive a confirmation email within two days. If not then
resend your solutions or contact the lecturer.) Before you start
working on the miniproject, read once again the instructions
concerning miniprojects on this page. Pay
special attention to the fact that the solutions must be your own solutions and solutions of different
groups must be independent.
In this miniproject you are asked to model and verify a realtime
mutual exclusion algorithm proposed by Rajeev Alur and Gadi Taubenfeld using
timed automata and Uppaal. The
algorithm is described in Section 11.3 of the latest version of
the textbook. The pseudocode for the algorithm is presented in
Table 11.1 on page 219.
Your tasks are as follows:
 Model the algorithm in Table 11.1 in Uppaal
for n=3 processes and Delta=2. Verify that it preserves mutual
exclusion. Increase the number of processes to four, and
repeat the verification.

Take the model you produced in your solution to the previous item,
and modify it so that at least one of the memory accesses of the
processes takes at most one time unit. Does the resulting algorithm
still preserve mutual exclusion? Experiment with different choices of
"fast steps". Do your conclusions depend on the steps that are
chosen to be "fast"?

Consider the variation of the algorithm by Alur and Taubenfeld offered
in Table 11.2. Model it using Uppaal for n=3 processes and Delta=2. Verify that it preserves
mutual exclusion.
How to deliver the miniproject?  Create a short
report. The report must be in pdf format and should contain:

Full names and emails at RU of all people that worked in your group
(maximum 3 students per group).
 Your commented implementation of
the variants of the algorithm.
 The formula in Uppaal syntax you
used for the specification of mutual exclusion.
 A short
conclusion about verification of the variants of the algorithm.
 A short report on your experience of working with Uppaal
The report does not have to be long at all but it should contain (at
least to some extent) all the points mentioned above.
Further Reading