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.
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.
horse: based on the example in Chapter 3. An intentionally
simple introductory exercise devised by Philippa Hopcroft.
variations on a puzzle about shunting trains
in timed specification and verification
variations on a puzzle, exercise in compression.
and verifying walking multi-part robots
themes from Section 4.2.1 of UCS
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 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.
is a page with some old slides based on the chapters of TPC.
You can contact the author via Bill.Roscoe
This site is
presently under construction