Second Mini Project

Modelling and Verification, Spring 2006


Modelling and Analysis of a Real-time Mutual Exclusion Algorithm

The deadline for delivering this mini-project 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 mini-project, read once again the instructions concerning mini-projects 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 mini-project you are asked to model and verify a real-time 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:
How to deliver the mini-project? Further Reading