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. 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.
- Hiding and divergence, the failures-divergences model.
- Specification and correctness.
- Communication, buffers, sequential composition.
Lecture Notes: The lecture notes for this year's course appear online on the course materials page.
- A. W. Roscoe, Understanding Concurrent Systems, Chapters 1-8, Springer 2010
- A.W. Roscoe, The Theory and Practice of Concurrency, Chapters 1-7, Prentice-Hall International, 1997; http://www.cs.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf.
- 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; http://www.computing.surrey.ac.uk/personal/st/S.Schneider/books/CRTS.pdf.
- S.D. Brookes and A.W. Roscoe. CSP: A practical process algebra: http://www.cs.ox.ac.uk/files/12724/cspfdrstory.pdf
Overheads: This year's slides will appear on the course materials page over the course of the term.