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.
Link to downloadable CSPM scripts from Roscoe's book: http://www.cs.ox.ac.uk/ucs/CSPM.html
Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.
Taking our courses
Matriculated University of Oxford students who are interested in taking this course, or others in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form. Priority will be given to students studying for degrees in the Department of Computer Science.