Module 02489 (2007)
Syllabus page 2007/2008
06-02489
Automatic Verification
Level 3/H
Manfred Kerber:5
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus
The Module Description is a strict subset of this Syllabus Page. (The University module description has not yet been checked against the School's.)
Relevant Links
NuSMV.
UPPAAL.
PRISM.
Verisoft.
Bogor.
GameChecker.
SDV.
Outline
The module introduces techniques and tools for verifying that computer systems have the properties intended. The module covers: reactive systems and their models; temporal logic; model checking and algorithms; a selection of tools; examples of systems (concurrent programs, communication protocols, embedded systems); verification of properties of systems (safety, liveness and fairness); the state explosion problem and approaches to it; symbolic model checking.
Aims
The aims of this module are to:
- introduce some methods and tools which have been developed in recent years for verifying properties of hardware and software systems
- look at examples, both small-scale ones for classroom demonstration, and large-scale ones in which verification has been successful
- understand the limitations of current tools, and how they may be overcome in the future
Learning Outcomes
| On successful completion of this module, the student should be able to: | Assessed by: | |
| 1 | use appropriate tools to verify and debug small-scale systems | Examination |
| 2 | understand and explain the principles and algorithms behind those tools | Examination |
| 3 | explain the application of the tools to the examples introduced | Examination |
| 4 | appreciate the limitations of current techniques and tools, such as the state explosion problem, and current efforts to overcome them | Examination |
Restrictions, Prerequisites and Corequisites
Restrictions:
None
Prerequisites:
None
Co-requisites:
None
Teaching
Teaching Methods:
18 hrs lectures, 7 hrs examples classes/practical sessions
Contact Hours:
Assessment
- Sessional: 1.5 hr examination (100%).
- Supplementary (where allowed): As the sessional assessment
Recommended Books
| Title | Author(s) | Publisher, Date |
| Systems and Software Verification: Model-Checking Techniques and Tools Symbolic model checking | Beatrice Berard et al | Springer, 2001 |
| Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed | M. Huth and M. Ryan | Cambridge University Press, 2004 |
| Model Checking | Edmund M. Clarke, Orna Grumberg, Doron A. Peled | The MIT Press, 2000 |
Detailed Syllabus
-
Introduction to model checking
- Reactive systems
- Transition system models
- Invariant and reachability checking
- The logic CTL
- CTL model checking
- Real-time and probabilistic systems
- Symbolic model checking and BDDs
- Software model checking
- Foundational issues
- Assertions
- Stateful models
- Predicate transformers
- Interaction models
- On-the-fly checking
- Abstraction and iterated refinement
Last updated: 7 Feb 2007
Source file: /internal/modules/COMSCI/2007/xml/02489.xml
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus