First Mini Project
Modelling and Verification, Spring 2006
Alternating Bit Protocol
The deadline for delivering this mini-project is Tuesday, 21 February, 2006 at
20:00. Deliver your solution via the intranet if you are a student at RU and via email
otherwise. (Those of you who deliver by email should receive 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.
The alternating bit protocol is a simple yet effective protocol for managing the
of lost messages. Consider a sender S and a receiver R, and assume that the
medium from S to R is initialized so that there are no messages in transit.
The alternating bit protocol works like this:
There is no direct communication between the sender and the receiver;
all messages must travel through the medium.
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
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.
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 below - using
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,
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
- 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 pdf format and
The report does not have to be long at all but it should contain (at least to some
extent) 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.
- Full names and emails at RU
of all people that worked in your group
(maximum 3 students per group).
- 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? ...).
- A brief description of the protocol including checksum is
- A graphical simulation of the protocol is available
(Note that the control bits in the acknowledgment of the messages are switched.)