Software Engineering - Systems Verification (303)
Lecturer: Dr Alessio
Lomuscio
Tutorials and labs: Dr Jonathan Ezekiel and Dr Maciej Szreter
Lecture Schedule
- Tuesday 14.00-15.00; room 144 (lecture).
- Thursday 16.00-17.00; room 145 (lecture).
- Thursday 17.00-18.00; room 145 (tutorial).
Course snapshot
The course is broadly divided into 5 parts:
- Specifications via logic-based languages (temporal and epistemic
logics) (about 6 hrs).
- Ordered binary decision diagrams and their manipulations (about
2 hrs).
- Model checking temporal/epistemic languages (about 4hrs).
- The SMV, Spin and MCMAS model checkers (about 4hrs).
- Advanced topics: bounded model checking, unbounded model
checking (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)
- 8 January.
- Introduction and motivation to the course including
learning
objectives, assessment methods. The specification and verification
problem in Software Engineering.
- 10 January.
- Modal specification languages: syntax and semantics.
- Tutorial 1
(syntax and satisfaction).
- 22 January.
- Validity, Completeness, and Axiomatisation for modal languages.
- 24 January.
- Temporal Logic: Linear Temporal Logic (LTL), Computational Tree
Logic (CTL).
- Tutorial 2 (Validity and correspondence exercises).
- 29 January.
- Temporal Logic: Expressivity in LTL and CTL. The logic CTL*.
- Formal methods, theorem proving and model checking.
- Specifications in LTL/CTL: the mutual exclusion problem.
- 31 January.
- Mutual exclusion revisited. Fairness. The Bit
Transmission Problem.
- Tutorial 3 (Satisfaction in LTL/CTL, mutual exlusion exercises).
- 5 February.
- Model Checking: The NuSMV language and toolkit.
- Tutorial 4: Specification patterns.
- 7 February.
- Going further: Temporal epistemic specifications.
- Tutorial 5: The NuSMV software toolkit (lab class 1).
- 12 February.
- The bit transmission problem.
- 14 February.
- Explicit model checking. Algorithms for LTL/CTL. State
explosion problem.
- Tutorial 6: NuSMV programming session (lab class 2).
- 19 February.
- Ordered Binary Decision Diagrams. Definitions and operations.
- 21 February.
- Model checking temporal epistemic specifications. The MCMAS
model checking toolkit.
- Tutorial 7: MCMAS programming session (lab class 3).
- 26 February.
- Symbolic Model Checking with OBDDs.
- 28 February.
- Bounded Model Checking.
- The Verics model checking toolkit.
- 4 March.
- Coursework Correction. Q&A session.
- Course wrap up. Course feedback.