First Mini Project
Semantics & Verification, Spring 2005
Alternating Bit Protocol
The deadline has now passed. Accepted reports are
here.
The deadline for delivering this mini-project is April 7th, 2005
via email to the lecturer. You should get a confirmation email within two 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.)
-
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.)