In this exercise you are asked to model 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.
Task 2: Validate the sytem in the simulator and find out what the total timed between "begin send" and "end receive" is.
Task 3: Modify the medium
M to handle messages of length length>=delay.
Exercise 2 (Modeling: the CSMA/CD Protocol continued)
In this exercise we use the model of the CDMA/CD protocol from the Lecture 2, Exercise 3. You are asked to refine the model so that the sent messages have a fixed length of time length, and to refine the communication medium M to have a communication delay of time delay.
Task 1: Model/modify the system with the assumption length<delay.
Task 2: Verify that the system is correct in the sense that all sent messages are indeed received..
Task 3: Refine the medium to allow messages of length length>=delay.
Task 4: Verify that the refined system is correct in the sense that all sent messages are indeed received.