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)
In
this exercise you will study the Media Access Control (Mac) sub layer of
the Carrier Sense, Multiple Access with Collision Detection (CSMA/CD) communication
protocol. The protocol specification consists of two MAC entities, MAC1
and MAC2, interconnected by a bi-directional
medium M. The MAC entities are identical
and can both transmit and receive messages over the medium. This means
that collisions may occur on the medium (if the two MAC's transmit simultaneously).
It is assumed that collisions will be detected in the medium and signaled
to both MAC1 and MAC2.
Overview of the MAC sub layer.
A model of the protocol is given in csma-cd-start.xta and csma-cd-start.ugi (the specification is taken from "Verifying a CSMA/CD Protocol with CCS" by Joachim Parrow. The specification uses the following synchronization actions to describe the protocol events:
- send - service provided by Mac which reacts by transmitting a message,
- rec - (receive) service provided by Mac, indicates that a message is ready to be received,
- b - (begin) Mac begins message transmission to M,
- e - (end) Mac terminates message transmission to M,
- br - (begin receive) M begins message delivery to Mac,
- er - (end receive) M terminates message delivery to Mac,
- c - (collision) Mac is notified that a collision has occurred on M.
MAC1.
Initially, MAC1 accepts a service call
(send1?). The MAC initiates transmission (b1!), unless a message is in
the process of being received. If the transmission is successfully terminated
(e1!) new messages can be transmitted and the process is repeated. If a
collision occurs (c1?) the MAC attempts re-transmission of the message.
In all states (except when a message is being transmitted) the MAC is willing
to start receiving. A message may be received (br1?) after which the MAC
may not begin message transmission before the end of message (er1?) has
been received and the MAC has signaled that the message is ready to be
delivered (rec1!). However, the MAC may receive a send request (send1?)
if there is not already another request waiting.
The medium M.
Initially, the medium accepts transmission
from one of the MAC's (b1? or b2?). We assume MAC1 (b1?) starts transmitting
first (the case for b2? is symmetric). The medium is assumed to be "half-duplex"
meaning that a full message must be transmitted (br2!, e1?, er2!) before
the next message can be accepted. If the receiving MAC (i.e. MAC2) starts
transmission (b2?) the medium interrupts the transmission and signals collision
(c1!, c2!) to both MAC1 and MAC1 (in any order).
Task 1: Open the protocol specification in csma-cd-start.xta and csma-cd-start.ugi, and add a test environment that "uses" the protocol. Validate that your system is functionally correct using UPPAAL's simulator.
Task 2: Check (by verification) if the system is correct in the sense that sent messages are received. How many messages can be in transfer at the same time? Is it 1, 2 or more messages?
Task 3: 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 4: Model/modify the system with the assumption length<delay and verify that the system is still correct in the sense that all sent messages are indeed received..
Task 5: Refine the medium to allow messages of length length>=delay and verify again that the refined system is correct in the sense that all sent messages are indeed received.