At the end of the course the student should:
- understand some of the issues and difficulties involved in Concurrency
- be able to specify and model concuurent systems using CSP
- be able to reason about CSP models of systems using both algebraic laws and semantic models
- be able to analyse CSP models of systems using the model checker FDR
- Processes and observations of processes; point synchronisation, events, alphabets. Sequential processes: prefixing, choice, nondeterminism. Operational semantics; traces; algebraic laws. 
- Recursion. Complete partial orders and fixed points as a means of explaining recursion; approximation, limits, least fixed points; guardedness and unique fixed points. 
- Concurrency. Hiding. Renaming. 
- Non-deterministic behaviours, refusals, failures; the determinism ordering. 
- Hiding and divergence, the failures-divergences model. 
- Specification and correctness. 
- Communication, pipes, buffers. Sequential composition. 
- Case study. 
Reading listCourse Text
- A. W. Roscoe, The Theory and Practice of Concurrency, Chapters 1-7, Prentice-Hall International, 1997.
- C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall International, 1985, http://www.usingcsp.com.
- S. A. Schneider, Concurrent and Real-time Systems, Chapters 1-8, Wiley, 2000.
Related research at the Department of Computer Science