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.
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.
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
Part 6. Advanced techniques. Limitations of current OBDD-based techniques. Bounded model checking. Abstraction. Refinement. More expressive specification languages: ATL, Strategy Logic.
Good knowledge of propositional and first-order logic.
No previous expertise on temporal logic nor formal verification is required.
Lectures, tutorials and programming labs
Coursework around week 5. Final exam.
2nd ed., Cambridge : Cambridge University Press
Cambridge, Mass. ; London : MIT Press
Istituto Scientifico per lo Studio e la Cura dei Tumori (IRST)