Teaching material

This page provides teaching material relevant to UCS and TPC.  This is the public page.  There will ultimately also be a private, password protected site that contains material only available to instructors such as solutions to exercises and practicals.

Practicals

Any course on CSP, except perhaps one on pure theory, should have the students do practical exercises in developing CSP descriptions of systems and specifications and trying these on a tool such as FDR.  The following are some practicals that the author has used.  These fall into two categories: ones that have been used together with courses on CSP, and ones that have been set as end-of-course  assignments to groups of software engineering students after a course on  FDR.

Pantomime  horse: based on the example in Chapter 3.  An intentionally simple introductory exercise devised by Philippa Hopcroft.

Shunting: solving variations on a puzzle about shunting trains

Timed Lift: Exercise in timed specification and verification

Lights out: Solving variations on a puzzle, exercise in compression.

Millepede: constricting and verifying walking multi-part robots

Reversible solitaire

Routing: developing themes from Section 4.2.1 of UCS

Non-blocking communications protocol: solving Exercise 4.13 of UCS.

Solutions to all of the above are available to instructors from the author.

Here is a page with some more puzzles the author has solved using FDR.


Slides

Slides to accompany teaching from the chapters of UCS will gradually be made available here.  The author frequently teaches the most tool-oriented material such as much of Chapter 8 by taking the audience through CSP files and running tools on them.

Chapter 1
Chapter 2
Chapter 3
Chapter 4
Chapter 5
Chapter 6
Chapter 7

Here is a page with some old slides based on the chapters of TPC.



You can contact the author via Bill.Roscoe (at) comlab.ox.ac.uk

This site is presently under construction