Teaching materials

This site provides material which has been used to teach an introductory course on untimed CSP at Royal Holloway, University of London. This material was originally produced by Simon Gay, with slight amendments by Steve Schneider. All material is available in postscript and in PDF format. It consists of slides for a sixteen lecture course, together with eight supplementary practicals.

Slides

The complete set of slides is available in postscript format.

Slides are also available by section in four to a page format for economical handouts:

Sequential Processes (postscript or PDF).
Concurrency (postscript or PDF).
Traces (postscript or PDF).
Specification; Abstraction (postscript or PDF).
Choice between processes (postscript or PDF).
Examples (postscript or PDF).
Refusals (postscript or PDF).
Failures (postscript or PDF).

Practicals

Using ProBe (postscript or PDF). Supporting CSP files: vm1.csp, vm2.csp, tickets.csp.
Parallel Processes (postscript or PDF). Supporting CSP files: student1.csp, independent.csp, prize.csp.
Using FDR (postscript or PDF). Supporting CSP files: spec1.fdr2, spec2.fdr2.
Specifications (postscript or PDF). Supporting CSP files: crossing.fdr2, peterson1.fdr2, peterson2.fdr2.
Internal Choice (postscript or PDF). Supporting CSP files: buses.csp.
Deadlocks (postscript or PDF). Supporting CSP files: dphil.fdr2, dphil_butler.fdr2.
The Cyclic Scheduler (postscript or PDF). No supporting CSP files.
Liveness Specifications (postscript or PDF). Supporting CSP files: crossing.fdr2, scheduler.fdr2.

All practicals are available in a single zipped postscript file.

All CSP files supporting practicals are also available in a single zip file.

Back to book home page