Specifying and verifying systems in CSP and FDR
Supervisor
Suitable for
Abstract
Choose some specific system; develop specifications and an implementation for it in CSP and relate these with FDR. Typical applications might include security, distributed algorithms and safety critical (including fault tolerant) systems. See Understanding Concurrent Systems Chapters 4, 8, 14, 15 and 20, and Theory and Practice of Concurrency Chapters 12 (security/fault tolerance), 14 and 15 for example case studies. [I would be particularly interested in case studies involving mobility or priority as described in Chapter 20.]Prerequisites: Concurrency