CS5270 Verification of Real Time Systems

Coursework marks so far:

None yet...

Lecturer:

Mr. Hugh Anderson
E-mail : hugh@comp.nus.edu.sg
Office : S15 - #06-12.
Consultation hours: Anytime - if my door is open. If it is closed - please knock. If I am at Spinellis getting a caffeine fix... sit down and have a chat.

Tutors:

TBA

Lectures:

The lectures are in S16, room 405, on Thursdays, from 1830 to 2030.

Text Book/Resources:

We will be using Hugh's course notes, and other papers as needed, available here.

Assessment:

Exam - open book (50%), Labs/Assignments(35%), Tests - closed book (15%)

Lecture notes:

You should read the notes for the lectures before attending the lecture!

Module 1 (lecture 1): Introduction. Please prepare by reading chapter 1 here in PDF, or here in postscript. The overheads are here There is also a more printable copy here - it uses less ink!

Module 2 (lecture 2): Hard real-time computing environment. Please prepare by reading chapter 2 here in PDF, or here in postscript. The overheads are here There is also a more printable copy here.

Module 3 (lecture 3): Scheduling. Please prepare by reading chapter 3 here in PDF, or here in postscript. The overheads are here There is also a more printable copy here.

Module 3 (lecture 4): Scheduling (Continued). The overheads are here There is also a more printable copy here. If you wish to read ahead and see what we will start on next week, I have put chapter 4 here in PDF, or here in postscript.

Module 4 (lecture 5): Transition systems. Please prepare by reading chapter 4. The overheads are here There is also a more printable copy here.

Module 4 (lecture 6): Transition systems. Please prepare by rereading chapter 4. The overheads are here There is also a more printable copy here.

Module 4 (lecture 7): Transition systems. There will be an exam! But also some lecture... so please prepare by rereading chapter 4. The overheads are here There is also a more printable copy here.

Module 4/5 (lecture 8): Zones and Model Checking. The overheads are here There is also a more printable copy here. I have put chapter 5 here in PDF, or here in postscript. We may get up to the first few pages of it...

Module 5 (lecture 9): Model checking. Please prepare by reading chapter 5. The overheads are here There is also a more printable copy here. Note that I have corrected the weird things happening on slide 31 with the left and right brackets...

Module 5/6 (lecture 10): Model Checking, CTL and TCTL. The overheads are here There is also a more printable copy here. I have put chapter 6 here in PDF, or here in postscript. We may get up to the first few pages of it...

Module 6 (lecture 11): Model Checking TCTL and Uppaal. The overheads are here There is also a more printable copy here.

Lecture 12: Seminar on RTL. The overheads are here.

Lecture 13: Seminar on TTA. The overheads are here.

Assignment:

Assignment 1: is here in PDF. Note that this assignment is due on 15th February despite what was indicated in lecture 3's slides...

Assignment 2: is here in PDF. Note that this assignment is due on 22nd March.

Assignment 3: is here in PDF. This is the last assignment, and is due on 9th April.