Formal Modelling and Analysis of Real-Time Systems: Lab 1
Part of the ARTES++ course Formella analysmetoder för realtidssystem (5p) VT'06.
Exercise 0
Installing the UPPAAL tool on your machine/accout. Note that the current
version of UPPAAL requires Java 1.5.
When unpacking the zip-file a directory named "demo" is created, which
contains a set of examples. It might be useful to look at them.
Exercise 1
In this exercise you are to model, simulate and verify a simple data link
protocol, where some unrealistic assumptions will be made in order to
keep the exercise simple.
The protocol specification is as follows: there is a Sender, a Receiver, and a Medium. The medium can after reception of a
message from the sender, do one of two things: either the message is
delivered to the receiver, or it is lost. When a message is lost a time-out in the sender will occur -
model this time-out as a communication signal sent from the medium (in
case of message loss) to the sender. In case of a time-out, the sender
will retransmit the message. When the receiver gets a message an
acknowledgment is sent to the sender. Assume that the acknowledgment is
sent directly to the sender and not through any medium.
Task 1: Model
the above protocol in UPPAAL, and validate using the simulator that it
is functionally correct.
Redefine the protocol by modifying the receiver so that it reports to
the layer above when a message is receive. Add a test process (to
model the above layer) that receives the messages from the
receiver. Modify the sender to receive messages from the layer
above. Add another test process that generates messages to the
sender (modeling the above layer).
Task 2: Validate that the functionality of the refined protocol
is correct using the simulator.
Now modify the test environment so that the test sender increments a
shared integer variable i whenever a message is sent. Modify the
test receiver so that it decrements the variable i whenever
a message is received.
Task 3: Validate the protocol and verify that the value of the
variable i is always one or zero.
Task 4: What happens if the protocol is redefined in the
following way: acknowledgments are not sent at all from the receiver to
the sender? What happens if additionally the sender never expects
acknowledgments? Simulate, verify and describe in words the behavior of
the resulting protocol.
Model the content of messages as (bounded) integer values and
change the models of the protocol and the test environment consequently.
Task 5: Validate and then verify, that the content of a message
when sent equals the content of the message when received.
Exercise 2
In this exercise you are asked to model and anlyse the the Alternating
Bit Protocl in UPPAAL.
Model the protocol as described in the Free
On-Line Dictionary of Computing. Do not model the
data or checksum of messages mentioned in the description. Model a
separate
Sender,
Receiver, and
Medium. Check the behaviour of your
model by simulation. You may also formulate and verify some correctness
properties of the protocol (e.g. like in the exercise above).
|