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:

• The introduction (Lecture 1) was not captured.
• The language of CSP: Lecture 2 (camera/screen), Lecture 3 (camera/screen) (no audio), Lecture 4 (camera/screen) (partial audio), Lecture 5 (camera/screen), Lecture 6 (recording unavailable)
• Trace semantics: Lecture 7 (recording unavailable), Lecture 8 (camera/screen), Lecture 9 (camera/screen), first half of Lecture 10 (camera/screen)
• Trace specification and verification: second half of Lecture 10 (camera/screen), Lecture 11 (camera/screen), Lecture 12 (camera/screen), Lecture 13 (camera/screen), first part of Lecture 14 (camera/screen)
• Stable failures: second part of Lecture 14 (camera/screen), Lecture 15 (camera/screen), Lecture 16 (camera/screen), Lecture 17 (camera/screen), part of Lecture 18 (camera/screen)
• Failures, divergence, and infinite traces: second part of Lecture 18 (camera/screen), Lecture 19 (camera/screen), Lecture 20 (camera/screen)
• Temporal logic and model checking: Lecture 21 (camera/screen), Lecture 22 (camera/screen), Lecture 23 (camera/screen) (also contains some remarks about putting everything together)

There are two videos for each recorded lecture, one featuring the camera feed and the other featuring a capture of the front desk screen. The audio track is the same for both videos. There aren't too many interesting things happening on the screen, so you should probably start with the camera stream combined with a separate view of the respective PDF lecture notes. Alternatively, you can to run both streams simultaneously (one of them muted).

Footnotes

... 7¹

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).

... note²

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).