Formal Modelling and Analysis of Real-Time Systems: Lab 2
Part of the ARTES++ course Formella analysmetoder för realtidssystem (5p) VT'04.
Exercise 1
In this exercise you are asked (again) to model and analyse a protocol
(but this time) with some real-time properties.
As indicated in the figure above, the system should consist of a
communication medium M, a
Sender, and a
Receiver.
The sender sends messages of a fixed length length, which is the time between the
beginning and the end of a message. The medium has a transmission
delay
delay, which is the time
between the beginning (or end) of a message is sent and the beginning
(or end) of a message is received. For example, if the beginning of a
message is sent at time t, it will be received by the receiver
at time t+delay.
Task 1: Model the system as a network of timed automata
in UPPAAL. Assume length<delay. Model the
beginning and end of each message. It is recommended to use
integer constants in UPPAAL for the values length and
delay.
The medium automata should not be needing the length
value to work correctly. Instead it only needs synchronize with
the other two automata using the b = begin send, e =
end send, br = begin receive and er = end
receive communication channels.
Task 2: Validate the system in the simulator and find
out what the total timed between begin send and end
receive is.
Task 3: Extend the medium M to also handle messages of
length length>=delay.
Exercise 2
In this exercise we study Fischer's Protocol for mutual
exclusion. We start out from the version shown below (where x
is a local clock and v a shared data variable).
Task 1: Formalise the three requirements below and use
the verifier of UPPAAL to check if they are satsified by the protocol:
-
mutual exclusion, i.e.
that there is never more than one process operating in its critical section
(modeled by location cs),
-
all processes can enter
their critical sections, and
-
a process is guaranteed
to enter its critical location within three time units.
Task 2: The protocol model is slightly inaccurate as the
processes can not leave the critical section. Refine the protocol to
allow processes to restart after having gained access to the critical
section and after having failed to gain access to the critical
section. Rerun the verification.
Task 3: The protocol model is still slightly inaccurate as a
process may stay too long in location b and may therefore not be
able to eventually reach the critical section. Modify the model so a
procuess must progress from location b (this may imply changing
the timing a bit on the existing edges).
Also, refine the protocol to model the fact that processes may, or may
not, be interested in accessing the critical section. Make sure that a
process is always allowed to eventually reach the critical section. Rerun
the verification of requirements 1 to 3 above. In addition, formalise and
prove that: if a process reaches location b it is guaranteed to
eventually reach location c.
| 
