02152 Concurrent Systems        Fall 2008
Thursday, September 18

Home

Plan

Material

<-prev

next->

Building 308, Auditorium 12

13.00-15.00

Workings of the SPIN verifier Liveness properties Survey of Temporal Logic [Some slides(ps)(pdf)] Weak and strong fairness Proving liveness properties Liveness in SPIN

Building 308, G-databar, rooms 15+16

15.00-17.00

CP Lab 3: Verification with SPIN

Texts and exercises

Today	Temporal logic: [Basic 4.1-4.3] (skim section 4.3) General Liveness: [Andrews 2.8] and [Basic 4.6] Liveness proofs in SPIN: [Spin 6]. You may optionally read about hand-proofs of liveness properties in [Basic  4.4-4.5].
Coming	Introduction to semaphores: [Andrews 4.1-4.2]. Semaphore invariant: [Basic 3.6].
Exercises	1. Do Exam Dec 1998, Problem 1, Questions 1.1 and 1.3 (in [Aux]) [You may also try to understand the proof lattice in Question 1.2]

Hans Henrik Løvengreen, Sep 18, 2008