Verification 6

Time:   23. May 2000

Litterature:

• (**) JPK chapter 4.
• (*)  Larsen, Pettersson, Yi: "UPPAAL in a Nutshell", in Journal for Software Tools for Technology Transfer, vol 1, 1997.
• (*) Rajeev Alur, David Dill: "Automata for Modeling Real-time Systems", in Proceedings of ICALP90.
• (*)   Rajeev Alur, Costas Courcoubetis, David Dill: "Model-Checking  for Real-Time Systems", In Proceedings of LICS90.
• (*)   Larsen, Steffen, Weise: "Continuous Modelling of Real Time and Hybrid Systems", inJournal for Software Tools for Technology Transfer, vol 1, 1997.
• (*)   Yi, Pettersson og Daniels: "Automatic Verification of Real-time Communicating Systems by Constraint-Solving", in proceedings of FORTE94.

Excercises:

• Exercise 32 in JPK.

• Model and analyze the following gossiping girls problem in UPPAAL. A number of girls initially know

     one distinct secret each. Each girl have 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).
     Only binary (between two girls in each phone call) is possible.

     Task 1: Use UPPAAL to find the minimal number of phone calls needed for four girls to know all
     secrets.

     Task 2: Try to find an (inductive) argument for how many phone calls are needed to solve the
     gossiping girls problem for n girls.

     Task 3: Refine your model so that each phone call requires start time units to connect, and in
     addition transfer time units to exchange each secret. Find the minimum time needed to solve the
     gossiping girls problem for four girls if start is 30 and transfer is 60.