Lecture Notes

The notes will be very sparse; I will only put in them definitions and the like (and maybe some worked, tedious exercises). The main matter will be discussed on the blackboard; these notes are just a mean to save me (and you too) some writing (and so some time).

Notes (handout) Notes (overhead presentation) Relevant textbook material
Introduction Introduction  
The language of CSP The language of CSP Part I
Traces Traces Chapter 4
Trace verification Trace verification Chapter 5
Stable failures Stable failures Chapter 6
Stable failure verification Stable failure verification Chapter 71
Failure, divergence, and infinite traces FDI Chapter 8
Model checking Model checking see note2
In place of conclusions In place of conclusions N/A

Lecture recording

My lectures are recorded, as follows:

Your preferences may vary, but for me the default viewing format (with a small PIP blackboard) does not work well. I therefore recommend that you switch the viewing mode to side-by-side. To switch the viewing mode click on the icon in the lower right corner of the video.


... 71
Failure trace testing was introduced in A Testing Theory for LOTOS using Deadlock Detection by Rom Langerak (in Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, North-Holland, 1989, pp. 87-98), which does not appear to be available on line. A brief summary is available in this paper (see Sections 2.2 and 2.3).
... note2
The presentation is largely according to Model Checking (by Clarke, Grumberg, and Peleg, MIT Press, 1999). The book is available in the Library (printed and also electronic versions, use the search feature on the Library's main page).