The aims of this module are to (1) present a collection of methods for dealing with software reliability; (2) explore in detail some of the methods and tools that have been developed in recent years for automatic verification of properties of software systems; (3) raise awareness to the limitations of current technologies, and how they may be overcome in the future.
This module introduces techniques and tools for verifying that computer systems are reliable in the sense that they have the properties intended. The module covers: languages for modelling systems and their properties; model checking and algorithms; a selection of tools (e.g. SPIN); specification, verification and validation of typical properties of reactive systems; limitations of automatic verification techniques; Relationship to software testing techniques (black-box checking).
Class sessions, tutorials and laboratory sessions together with
course notes, recommended reading, worksheets, printed solutions,
and some additional hand-outs.
Assessed coursework, traditional written examination.
To teach students the role and nature of software reliability methods; to develop in the students the ability to separate concerns during system verification, namely in what concerns modelling software systems, specifying required properties, and applying model-checking based verification techniques.
On completion of this module, the student should be able to:
use tools (e.g. SPIN) to verify and debug small-scale systems; understand and explain the principles and algorithms behind those tools; understand the application of the tools to different domains; understand the limitations of current verification techniques (e.g. the state explosion problem) and efforts to overcome them.
Class sessions together with worksheets.
Explanation of Pre-requisites
Knowledge of Discrete Maths will be helpful.
Software reliability methods are now past the stage of "promising curiosities" and offer techniques and tools that can be employed in a variety of application domains to verify required functional properties against models of system behaviour.
- Modelling Software systems with state transition systems.
- Specifying software system properties with temporal logic.
- Automatic verification techniques based on model-checking.
- Combining model-checking with black-box testing.
Study guide, worksheets, lecture rooms with data projector,
computer laboratory access, tutorial rooms with OHP.
Course questionnaires, course review.
Author: N. Rahman, tel: +44 (0)116 252 2593
Last updated: 2004-09-29
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.