Systems Verification (303)
Lectures: Prof.
Alessio Lomuscio
Tutorials: Mr Michael Akintunde, Ms Yi-Ling Liu, Prof Alessio
Lomuscio, Mr Edoardo Pirovano.
Lecture Schedule
- Monday 2pm-4pm; room 311.
- Wednesday 9am-11am; room 144.
Course summary
The course is broadly divided into 5 parts:
- Specifications via logic-based languages (temporal and
epistemic logics) (approx. 4 hrs).
- Ordered binary decision diagrams and their manipulations
(approx. 4 hrs).
- Model checking temporal/epistemic languages (approx. 6hrs).
- The NuSMV and MCMAS model checkers (approx. 4hrs).
- Bounded model checking, parameterised model checking (approx.
4hrs).
The topics will be covered in succession and will be accompanied by
tutorial classes and labs as appropriate. There will be one assessed
coursework around week 4.
The above is subject to slight changes.
Material
Lecture slides and tutorials (with solutions) will be provided on
CATE.
An excellent reference text book for most of the material of the
course is M Huth, M Ryan, Logic in Computer Science. Particularly we
will cover material in chapters 3, 4 and 6.
The book is also directly used in many examples in the lectures and
exercises.
The slides and exercise notes used in class are copyrighted.
They can be freely downloaded and used for revision for students
attending the present course but cannot be used by third parties
without the lecturer's permission.
Detailed course breakdown
(This year's module was considerably shortened)
- 17 January
- Introduction and motivation to the course including learning
objectives, assessment methods. Overview of the course.
- Modal specification languages: syntax and semantics.
- Tutorial 1 (modal syntax and satisfaction).
- 22 January
- Linear Temporal Logic (LTL)
- Tutorial 2 (LTL).
- 24 January
- Branching Time Temporal Logic (CTL).
- Exercises from Tutorial 2 (CTL).
- 29 January
- Temporal Specifications, Temporal Equivalences.
- Tutorial 3 (Temporal Specifications).
- 5 February
- Temporal Specifications.
- Mutual Exclusion Problem.
- The Bit Transmission Problem.
- Coursework.
- 7 February
- Explicit Model Checking.
- Tutorial 4 (Explicit model checking).
- 12 February
- Binary Decision Diagrams.
- Tutorial 5 (Binary Decision Diagrams).
- 14 February
- Symbolic Model Checking.
- The NuSMV model checker.
- 19 February
- Temporal Epistemic Specifications.
- The Bit Transmission Problem revisited.
- 21 February
- Tutorial 6-7 (The NuSMV model checker) - labs - 2hrs.
- 7 March
- The MCMAS model checker.
- Tutorial 8 (Epistemic Specifications)
- 12 March