Module 02489 (2002)

Syllabus page 2002/2003

06-02489
Automatic Verification
Level 3/H

:5
Mark Ryan (coordinator)
10 credits in Semester 1

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

Notes for Dr Ryan's section (also available from the lecturer).
Notes for Dr Kwiatkowska's section (also available from the lecturer).
The SMV manual.
The SMV home page. smv is installed locally on the Suns (e.g., dipsy), in /bham/ums/solaris/pd/packages/smv/smv. The examples are in /bham/ums/solaris/pd/packages/smv/examples/.
The CSP archive
FDR2 home page. fdr2 is installed locally on the Suns, as /bham/com/bin/fdr2. Examples are in /bham/com/packages/fdr-2.27/demo.
The FDR2 manual
ProBE home page. probe is installed locally on the Suns, as /bham/com/bin/probe. Examples are in /bham/com/packages/fdr-2.64/demo/.
The ProBE manual will be found at /bham/com/packages/probe-1.25/manual/probe.ps.
Other tools for concurrent systems (for interested students) are:
The Edinburgh Concurrency Workbench (available on our Unix system).
SPIN (available on our Unix system)
LOTOS (not available)

Outline

The module introduces techniques and tools for verifying that computer systems have the properties intended. The module covers: languages for modelling systems and their properties; Model checking and algorithms; A selection of tools (e.g. SMV, SPIN and FDR); Examples of systems (lifts, telephone systems, distributed systems and communication protocols); Verification and validation 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 for verifying systems 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:
1Use the tools SMV and FDR2 to verify and debug small-scale systems. Examination
2Understand and explain the principles and algorithms behind those tools Examination
3Explain the application of the tools to the examples introduced: communications protocols, lift system, process networks, cache coherency, telecommunication systems. Examination
4Appreciate 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:

25

Assessment

  • Supplementary (where allowed): As the sessional assessment
  • 2 hr examination (100%).

Recommended Books

TitleAuthor(s)Publisher, Date
Logic in Computer Science: Modelling and Reasoning about SystemsM. Huth and M. RyanCambridge University Press, 2000
Symbolic model checkingK. McMillanKluwer Academic Publishers, 1993
The Theory and Practice of ConcurrencyA. W. RoscoePrentice Hall, 1997
Concurrent and real-time systems: the CSP approachSteve SchneiderJohn Wiley and sons, 1999
Design & validation of computer protocolsG. HolzmannPrentice Hall, 1991

Detailed Syllabus

  1. Model checking: the SMV system.
    • Introduction to verification and model checking.
    • Temporal logic.
    • Model checking.
    • The SMV system.
    • Examples: communication protocols; the lift system.
    • Fairness.
    • Symbolic model checking and BDDs
  2. CSP and the FDR system.
    • Protocol Design and Validation. Ping-pong protocol and Alternating bit protocol with timeouts.
    • Simple CSP Processes.
    • Concurrency in CSP.
    • CSP Rules. Concurrent Processes.
    • Process Networks in CSP. Sorter example.
    • Specification and verification.
    • Case Study: Cache Coherency. From CSP notation to FDR.

Last updated: 29 July 2001

Source file: /internal/modules/COMSCI/2002/xml/02489.xml

Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus