In this exercise you are to model, validate 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 are 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. The loss of a message should be modeled by an internal transition (unlabelled transition in UPPAAL), since the loss itself does not constitute an observable event. 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? Validate, 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 afterwards verify, that the content of a message when sent equals the
content of the message when received.
Exercise 2 (Theory)
JPK exercises 17,
18, 22.
Exercise 3 (Modeling, The CSMA/CD Protocol)
In
this exercise you will study the Media Access Control (Mac) sub layer of
the Carrier Sense, Multiple Access with Control 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?
The model of the MAC is slightly inaccurate. In reality, a MAC would be two processes: one sender performing the actions send!, b!, e!, c? and one receiver performing the actions rec!, br? and er?
Task 3: Refine the protocol by letting each MAC consist of two processes, a sender (S) and a receiver (R). The idea is to let S perform all "horizontal" transitions and R all "vertical" transitions. Replace MAC with S and R. Use UPPAAL to validate and verify that the protocol no longer is correct.
Task 4: Redefine the protocol again
so that it works, while still keeping the S and R separate. This is a bit
tricky. You may need to add some synchronization channels (or data variables)
to achieve synchronization between S and R.