Mini Project

Modelling and Verification

Alternating Bit Protocol

The deadline for delivering this mini-project is Friday, 14 November, 2008 at 12:00. Deliver your solution via email. (You should receive a confirmation email within two days. If not then resend your solutions or contact me.) 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: