Supervisor

Suitable for

Abstract

The aim of this project is to model distributed algorithms or protocols using the process algebra CSP, and then to analyse them using the model checker FDR~[1].

The choice of algorithms to analyse would be up to the student, but here are some possibilities:

• the Session Initiation Protocol (SIP), a signalling protocol for Internet telephony[2]
• common communication protocols such as those in the ISO OSI or TCP/IP models[3], or the i-Protocol[4];
• asynchronous hardware;
• feature interaction[5].

The Concurrency course would be a prerequisite.

References

1. A. W. Roscoe, The Theory and Practice of Concurrency, > >Prentice Hall, 1997.
2. SIP: Session Initiation Protocol
3. A. S. Tanenbaum, Computer Networks, Prentice Hall, 1996.
4. i-Protocol
5. FIREworks home page