Real-Time Systems

Lecture 5

Subject

UPPAAL's Modeling Language
UPPAAL's Specification Language
The Bounded Retransmission Protocol

Material

JPK section 4.9.
UPPAAL in a Nutshell.

Slides.
UPPAAL model (and partial q-file) of the Bounded Retransmissin Protocol.

Exercises

Exercise 1

Consider the above system, where a SENDER and a RECEIVER wants to communicate over a potential faulty communication line.  In order to allow the SENDER to detect when communication succeeds, two (potentially faulty) communication media are used: one (K) for transmitting the message from SENDER go RECEIVER and one (L) for transmitting acknowledgements from the RECEIVER to the SENDER.  We assume that the both media are one-place buffers.  Also, we shall pay no attention to the actual message being communicated.

Use UPPAAL to model and analyse communication systems of the above type, where the media

• are lossy
• have delays

The desired behaviour of the overall system is that of a one-place buffer.  Use UPPAAL to examine to what extent this behaviour is meet in the various scenarios above.

Exercise 2

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.