Systems Verification

Module aims

 The course is an introduction to the area of formal methods for system specification and verification. Particular prominence is given to logic-based formalisms and techniques, notably model checking. Symbolic model checking via ordered-binary decision diagrams is covered in some detail and so are alternative techniques including bounded model checking and abstraction.

Learning outcomes

 Upon the successful completion of this module the student will be able to: 
1) Understand the use of temporal logic and epistemic logic as a formal specification language. 
2 Understand and use sophisticated verification algorithms for the verification of computing systems such as the ones based on ordered-binary-decision diagrams and SAT-based approaches.
4) Become proficient in the use of a mainstream model checking toolkit (such as nuSMV) to verify systems against complext specifications.  
5) Appreciate the limitations of the current tools and techniques and develop a basic understanding of current research directions.

Module syllabus

Part 1: Introduction. Why verification and validation. Verification in the Software-engineering life-cycle. Correctness, Faults and Errors. Lessons learnt:  Arianne V, London Ambulance Service, etc. Automated theorem proving: pros and cons. Model checking pros and cons. 

Part 2: Logics and specifications. Temporal logic. LTL. CTL. Expressive power. Epistemic logic, interpreted systems. Specifications in  temporal and epistemic logic. Examples: mutual exclusion, the bit transmission problem, the dining cryptographers protocol.

Part 3: Verification. Theorem proving and model  checking. Explicit and symbolic model checking. Boolean  formulas. Ordered-binary-decision-diagrams. Fixed point  operators. Protocol design and verification. Verification of epistemic specifications.


Part 4. Model checking packages: The NuSMV model checking  toolkit. The MCMAS Model checker. SMV and ISPL syntax. Hands on lab classes on automatic verification including debugging and validating protocols. Countermodels. 

Part 5. Verification Scenarios. Verification of security protocols (anonymity and 
authentication).

Part 6. Advanced techniques. Limitations of current OBDD-based  techniques. Bounded model checking. Abstraction. Refinement. More expressive specification languages: ATL, Strategy Logic.

Pre-requisites

Good knowledge of propositional and first-order logic. 

No previous expertise on temporal logic nor formal verification is required.

 

Teaching methods

Lectures, tutorials and programming labs

Assessments

Coursework around week 5. Final exam.

Reading list

Core Reading

Module leaders

Professor Alessio Lomuscio