Skip to main content

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