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 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: There is no direct communication between the sender and the receiver; all messages must travel through the medium.

Your tasks are as follows:
How to deliver the mini-project? Useful links: