Case studies with CSP and FDR
|
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
- A. W. Roscoe, The Theory and Practice of Concurrency, > >Prentice Hall, 1997.
- SIP: Session Initiation Protocol
- A. S. Tanenbaum, Computer Networks, Prentice Hall, 1996.
- i-Protocol
- FIREworks home page