Software Engineering - Systems Verification (303)
Lecturer: Dr Alessio
Lomuscio
Course Support Leader: Dr Mika Cohen
Tutorials: Jonathan Ezekiel and Dr Mika Cohen
Lecture Schedule
- Thursday 10.00-11.00; room 145 (lecture).
- Thursday 14.00-15.00; room 145 (lecture).
- Thursday 15.00-16.00; room 145 (tutorials).
Course snapshot
The course is broadly divided into 5 parts:
- Specifications via logic-based languages (temporal and epistemic
logics) (about 4 hrs).
- Ordered binary decision diagrams and their manipulations (about
4 hrs).
- Model checking temporal/epistemic languages (about 4hrs).
- The NuSMV and MCMAS model checkers (about 4hrs).
- Advanced topics: bounded model checking, abstraction, symmetry
reduction (about 2hrs).
The topics will be covered in succession and will be accompanied by
tutorial classes and labs as appropriate. 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 part of the course will be
updated throughout the course)
- 21 January.
- Introduction and motivation to the course including
learning
objectives, assessment methods. The specification and
verification problem in Software Engineering.
- Modal specification languages: syntax and semantics.
- Tutorial 1 (syntax and modal satisfaction).
- 28 January.
- Linear Temporal Logic (Syntax and Semantics)
- Computation Tree Logic (Syntax and Semantics)
- Expressive Power in LTL, CTL. CTL*.
- Tutorial 2 (satisfaction in LTL and CTL).
- 4 February.
- Model checking vs Theorem Proving in Temporal Logic.
- Mutual Exclusion in LTL and CTL.
- Tutorial 3 (specifications and mutual exclusion).
- 11 February.
- Lecturer's illness - lectures cancelled.
- 18 February.
- Epistemic specifications.
- Model checking with NuSMV
- Tutorial 4 (Lab session: Model checking with NuSMV - session 1).
- 25 February.
- Explicit model checking algorithms.
- BDTs, BDDs, OBDDs, ROBDDS.
- Tutorial 5 (Lab session: Model checking with NuSMV - session 2).
- 4 March.
- Symbolic Model checking with OBDDs.
- Model checking with MCMAS.
- Tutorial 6 (Lab session: Model checking with MCMAS - session 1).
- 11 March.
- Bounded Model Checking.
- Java Path Finder and BDD-based BMC (Andrew V Jones)
- Coursework correction.
- Tutorial 7 (Lab session: Model checking with MCMAS - session 2).
- 12 March.
- Corrected coursework pick up from Room 344.
- 18 March.
- Abstraction (Mika Cohen)
- Symmetry Reduction (Mika Cohen)
- Tutorial 8 (Abstraction and Symmetry).
- Course wrap up (2pm, room 343).