Second Mini Project
Semantics & Verification, Spring 2005
Gossiping Girls
The deadline has now passed. Accepted reports are
here.
The deadline for delivering this mini-project is April
29th, 2005,
via email to the lecturer. You should get 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 analyze the following gossiping girls problem in UPPAAL.
A number of girls initially know one distinct secret each. Each girl has
access to a phone which can be used to call another girl to share their
secrets. Each time two girls talk to each other they always exchange
all secrets with each other (thus after the phone call they both know
all secrets they knew together before the phone call). The girls
can communicate only in pairs (no conference calls) but it is possible
that different pairs of girls talk concurrently.
Your tasks are as follows:
- Model the problem as a network of UPPAAL timed automata
and use UPPAAL to find the minimal number of phone calls needed
for four girls to know all secrets.
- Refine your model so that each phone call lasts exactly 60 seconds
(for simplicity this time duration is irrelevant of the number of
exchanged secrets).
Find the minimum time needed to solve the gossiping girls problem
for four girls.
- Experiment with the UPPAAL search options breath-first and depth-first
search and with the diagnostic trace settings fastest and shortest. Try
to solve the problem for five girls.
Hints:
- Design a single template for all girls.
- For each girl, remember the currently known secrets in a local
integer variable (use a binary encoding such that if a girl knows
the secrets of e.g. girls 1 and 3 but does not know the secrets of
girls 2 and 4, the value in the integer variable will be
(0101) binary = 5; you might find useful the operation | for a
bitwise OR).
- In order to model value passing when two girls make a phone call,
you might want to read section 6.2 in "A Tutorial on UPPAAL", available
online.
How to deliver the mini-project?
- Create a very short report. The report must be in a pdf format and
should contain:
- Full names, emails at AAU and student numbers
of all people that worked in your group
(maximum 3 students per one group); repeat the
same information also
in the text of the email
that you send to the lecturer for easy copy and paste
of this data.
- A snapshot from the UPPAAL tool showing the template that describes
a girl.
- Summary of your verification results (minimal number of calls
for 4 girls; minimal time for 4 girls).
- A short conclusion where you might want to hint whether you managed
to find a diagnostic trace for 5 girls and what do you think about the
complexity of solving the problem. What was your experience when
working with UPPAAL?
- Send the report together with the UPPAAL source file
via email to the lecturer.