Concurrency: 2008-2009
Lecturer | |
Degrees | Part A Core — Computer Science Part A — Mathematics and Computer Science ECS Part I — MEng Engineering and Computing Science |
Term | Michaelmas Term 2008 (16 lectures) |
Overview
Learning outcomes
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
Synopsis
- Processes and observations of processes; point synchronisation, events, alphabets. Sequential processes: prefixing, choice, nondeterminism. Operational semantics; traces; algebraic laws. [3]
- Recursion. Complete partial orders and fixed points as a means of explaining recursion; approximation, limits, least fixed points; guardedness and unique fixed points. [1]
- Concurrency. Hiding. Renaming. [3]
- Non-deterministic behaviours, refusals, failures; the determinism ordering. [2]
- Hiding and divergence, the failures-divergences model. [1]
- Specification and correctness. [2]
- Communication, pipes, buffers. Sequential composition. [2]
- Case study. [2]
Syllabus
Reading list
Course 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
Activities |
Taking our courses
This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses
Other matriculated University of Oxford students who are interested in taking this, or other, courses 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.