Appendix A - Suggestions for student projects

Summary

This appendix describes three selected student projects. All these projects involve the use of software tools for verification and validation. In our lecture courses we have usually introduced the students to the Concurrency Workbench (CWB) and to Uppaal, but other tools could be used just as well. Further information on the following projects and more suggestions for student projects are available from the web page for the book at www.cs.aau.dk/rsbook/.

Alternating-bit protocol

In this project you are asked to model the alternating-bit protocol in the CCS language and verify your model using the 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 as follows.

• Each message sent by S contains an additional protocol bit, 0 or 1.

• When S sends a message, it does so repeatedly (with its corresponding bit) until it receives an acknowledgment (ACK) from R that contains the same protocol bit as the message being sent.

• When R receives a message, it sends an acknowledgment ACK to S and includes the protocol bit of the received message. 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.