Semantics & Verification, Spring 2008

First Mini Project

Semantics & Verification, Spring 2008

Alternating Bit Protocol

The list of accepted mini-projects is now available here. If you think your number should be on the list and it is not, inform the lecturer (Jiri) as soon as possible.
If you would like to get some feedback on your solution, please, send an email to Jiri and agree on a meeting.

The deadline for delivering this mini-project is 23:59 on Monday, March 17th, 2008 via email to the lecturer (Jiri). You should get a confirmation email within two working days. If not then resend your solutions or contact the lecturer. Before you start working on the mini-project, read once again the instructions concerning mini-projects on this page. Pay special attention to the fact that the solutions must be your own solutions and solutions of different groups must be independent.

In this mini-project you are asked to model the alternating bit protocol in the CCS language and verify it using CWB. Alternating bit protocol is a simple yet effective protocol for managing the retransmission of lost messages. Consider a sender S and a receiver R, and assume that the communication medium from S to R is initialized so that there are no messages in transit. The alternating bit protocol works like this:

Each message sent by S contains an additional protocol bit, 0 or 1.
When S sends a message, it sends it repeatedly (with its corresponding bit) until receiving an acknowledgment (ACK) from R that contains the same protocol bit as the message being sent.
When R receives a message, it sends an ACK to S and includes the protocol bit of the message received. When a message is received for the first time, the receiver delivers it for processing, while subsequent messages with the same bit are simply acknowledged.
When S receives an acknowledgment containing the same bit as the message it is currently transmitting, it stops transmitting that message, flips the protocol bit, and repeats the protocol for the next message.

There is no direct communication between the sender and the receiver, all messages must travel through the medium.

Your tasks are as follows:

Implement the alternating bit protocol in CWB. (Abstract away from the content of the messages and focus only on the additional control bit. To model the decision when the sender retransmits the message, use either nondeterminism or ever better a special process called Timer which will communicate with the sender on a channel called timeout and thus signal when a message should be retransmitted. You can also try to model the checksum verification - see the link bellow - using nondeterminism.) Hint: Take a look at slides in Lecture 4 where a similar (simpler) protocol was described.
Suggest a specification of the protocol and check whether it is equivalent to your implementation (use a suitable equivalence notion available in CWB). In particular, consider the following degrees of reliability of the communication medium and answer this question for all of these choices:
- perfect channels (all received messages are delivered)
- lossy channels (received messages can get lost without any warning)
- lossy and duplicating (in addition the received message can be delivered several times).
Check for possible deadlocks (stuck configurations) and livelocks (a possibility of an infinite sequence of tau actions) by formulating the properties as recursive formulae and by verifying whether the implementation satisfies these formulae.

How to deliver the mini-project?

Create a short report. The report must be in the pdf format and should contain:
- full names, emails at AAU and student numbers of all people that worked in your group (maximum 3 students per one group); repeat the same information also in the text of the email that you send to the lecturer for easy copy and paste of this data
- your commented implementation and specification of the protocol (suggestion: use * for the comments in the protocol description and then copy/paste it directly into the report)
- a short conclusion about verification of the protocol using equivalence checking (including perfect, lossy, and lossy and duplicating channels), what equivalence did you choose and why?
- formulae in CWB syntax for deadlock and livelock and whether your implementation does or does not satisfy these formulae
- a short conclusion (e.g. Does the protocol satisfy the desired properties? What are the possible extensions of the protocol or do you have any suggestions for a more advanced modelling of some features of the protocol? What was your experience when working with CWB? ...)
The report does not have to be long at all but it should contain (at least to some extend) all the points mentioned above. Send the report together with the CWB source file containing the implementation and specification of the protocol via email to the lecturer.

Useful links:

A brief description of the protocol including checksum is here.
A graphical simulation of the protocol is available here. (Note that the control bits in the acknowledgment of the messages are switched.)