Project Assignment

This page describes two project assignments that are part of the ARTES++ course Formella analysmetoder för realtidssystem (5p) VT'04. You are requested to complete one of the project assignments, corresponding to two credit points of work.

Alternative 1: Define your own project!

It must be possible to model the problem in some model-checking tool, and the model should be checked to satisfy a formal specification. Of course, you are most welcome to use other tools than UPPAAL.

If you wish to define you own project, write a short description of the problem and email it (in plain text of pdf) to us. Remember to describe the problem, how you plan to solve the problem, and which tool you will use.

Alternative 2: Modeling and Analysis of a Bounded-Retransmission Protocol

This problem is intended for students that do not define their own project assignment (as described above). The project is to model, validate and verify a concurrent system where timing is important for the correctness of the system behavior, using a software tool so that you will get some experience with formal description and verification techniques.

You may choose any of your favorite tools for the project. But if you need assistance during the project, we would recommend UPPAAL. In the next section there is an informal description of a Bounded Retransmission Protocol (BRP) for large data packets, it is a real protocol implemented in some Philips' equipment. The properties to check are described in a separate section together with some assumptions and hints for the assignment.

Informal Protocol Description

The protocol serves for the transmission of large data packets over unreliable channels. It splits each data packet and transmits it in parts. In case of failure of transmission, only a limited number of retries are allowed (bounded retransmission), hence the protocol may give up the delivery of a part of the packet. Both the sending and the receiving client are informed adequately. The protocol is used in one of Philips' products. External behaviour of the BRP As any transmission protocol, the BRP behaves like a buffer, i.e. it reads data from one client to be delivered at another one. There are two distinguishing features that make the behaviour much more complicated than a simple buffer. Firstly, the input is a LARGE DATA PACKET (that can be modeled as a list), which is delivered in small chunks. Secondly, there is a LIMITED AMOUNT OF TIME for each chunk to be delivered, so we cannot guarantee an eventually successful delivery within the given time bound. It is assumed that either an initial part of the list or the whole list is delivered, so the chunks will not be garbled and their order will not be changed. Of course, both the sender and the receiver want an INDICATION whether the whole list has been delivered successfully or not. The input (the list l = d_1,...,d_n) is read on the "input" port. Ideally, each d_i is delivered on the "output" port. Each chunk is accompanied by an indication. This indication can be I_FST, I_INC or I_OK. I_OK is used if d_i is the last element of the list. I_FST is used if d_i is the first element of the list AND MORE WILL FOLLOW. All other chunks are accompanied by I_INC. However, when something goes wrong, a "not OK" indication (I_NOK) is delivered without datum. Note that the receiving client does not need a "not OK" indication before delivery of the first chunk nor after delivery of the last one. The sending client is informed after transmission of the whole list, or when the protocol gives up. An indication is sent out on the "input" port. This indication can be I_OK, I_NOK or I_DK. After an I_OK or an I_NOK indication, the sender can be sure, that the receiver has the corresponding indication. A "don't know" indication I_DK may occur after delivery of the last-but-one chunk d_{n-1}. This situation arises, because no realistic implementation can make sure whether the last chunk got lost. The reason is that information about a successful delivery has to be transported back somehow over the same unreliable medium. In case the last acknowledgement fails to come, there is no way to know whether the last chunk d_n has been delivered or not. After this indication, the protocol is ready to transmit a subsequent list. Description of the protocol The protocol consists of a sender S equipped with a timer T1, and a receiver R equipped with a timer T2 that exchange data via two unreliable (lossy) channels, K and L. SENDER S reads a list to be transmitted and sets the retry counter to 0. Then it starts sending the elements of the list one by one over K to R. Timer T1 is set and a frame is sent into channel K. This frame consists of three bits and a datum. The first bit indicates whether the datum is the first element of the list. The second bit indicates whether the datum is the last item of the list. The third bit is the so-called alternating bit, that is used to guarantee that data is not duplicated. After having sent the frame, the sender waits for an acknowledgement from the receiver, or for a timeout. In case an acknowledgement arrives, the timer T1 is reset and (depending in whether this was the last element of the list) the sending client is informed of correct transmission, or the next element of the list is sent. If timer T1 times out, the frame is resent (after the counter for the number of retries is incremented and the timer is set again), or the transmission of the list is broken off. The latter occurs if the retry counter exceeds its MAXimum value. RECEIVER R waits for a first frame to arrive. This frame is delivered at the receiving client, timer T2 is started and an acknowledgement is sent over L to S. Then the receiver simply waits for more frames to arrive. The receiver remembers whether the previous frame was the last element of the list and the expected value of the alternating bit. Each frame is acknowledged, but it is handed over to the receiving client only if the alternating bit indicates that it is new. In this case timer T2 is reset. Note that (only) if the previous frame was last of the list, then a fresh frame will be the first of the subsequent list and a repeated frame will still be the last of the old list. This goes on until T2 times out. This happens if for a long time no new frame is received, indicating that transmission of the list has been given up. The receiving client is informed, provided the last element of the list has not just been delivered. Note that if transmission of the next list starts before timer T2 expires, the alternating bit scheme is simply continued. This scheme is only interrupted after a failure. TIMER T1 times out if an acknowledgement does not arrive "in time" at the sender. It is set when a frame is sent and reset after this frame has been acknowledged. (Assume that premature timeouts are not possible, i.e. a message must not come AFTER the timer expires.) TIMER T2 is (re)set by the receiver at the arrival of each new frame. It times out if the transmission of a list has been interrupted by the sender. So its delay must exceed MAX times the delay of T1. Assume that the sender does not start reading and transmitting the next list before the receiver has properly reacted to the failure. This is necessary, because the receiver has not yet switched its alternating bit, so a new frame would be interpreted as a repetition.

The assignment

Requirements

1. It is possible to send a whole file.
2. The buffers, K and L, will never overflow.
3. The specification is Deadlock-free.
4. There is never a data packet and an acknowledgement in transfer simultaneously. (This property justifies the fact that one channel could have been used instead of two.)
5. The sending and the receiving client must be consisten in their indication.
6. The sending and the receiving client will only indicate success if the whole file was transfered. Also, they must not indicate error if the whole file was successfully transfered.
7. It is not possible for the sender to start sending a packet before the previous sent packet is received.
8. The sending and receiving clients will eventually stop sending/receiving the file.
9. Eventually the file transfer will complete, or an error will occur in the sender.
10. A receiving client will eventually receive a complete file or indicate an error (NOK).

Also argue why all timeout values are appropriate with respect to other delays in the system.

The project report

You may solve the assignment individually or in groups of two. In the latter case, of course both must actively participate in the work and be able to motivate every step in your solution.