ARTES
-------------------------------------------------

 

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).

  ---------------------line----------------------------
  Strategic Research