Systems Verification (303)
Lectures: Prof.
Alessio Lomuscio
Tutorials: Dr Ioana Boureanu; Mr Panagiotis Kouvaros
Lecture Schedule
- Monday 11.00-13.00; room 145.
- Friday 11.00-13.00; 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, abstraction, refinement (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 schedule will be updated throughout the course)
- 18 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 (Syntax and Semantics)
- Tutorial 2 (satisfaction in LTL)
- 25 January.
- Computation Tree Logic (Syntax and Semantics)
- Tutorial 2 (satisfaction in CTL)
- 29 January.
- Expressive Power in LTL and CTL. CTL*
- Systems Specifications in Temporal Logic.
- Specifications for the Mutual Exclusion Problem.
- 1 February.
- Further Modelling Examples. The Mutual Exclusion Problem
revised. The Bit Transmission Problem. Fairness.
- Tutorial 3 (Specification patterns).
- 5 February.
- Model checking algorithm for CTL. Complexity.
- Binary Decision Trees and Binary Decision Diagrams.
- Coursework Set.
- 8 February.
- Symbolic Model Checking with OBDDs.
- Tutorial 4 (Explicit Model Checking and OBDDs).
- 12 February
- The NuSMV model checker.
- Tutorial in the Labs (NuSMV).
- 15 February
- Tutorial in the Labs (NuSMV).
- Epistemic Specifications.
- 19 February
- Analysis of The Bit Transmission Problem via Epistemic
Specifications.
- The model checker MCMAS.
- 22 February
- Tutorial MCMAS in the labs (2hrs).
- 26 February
- Bounded Model Checking.
- Tutorial 9: Epistemic Specifications.
- 29 February
- Parameterised Model Checking.