Department of Computer Science
	MSc Course-work

Dependable Systems Case Study

Introduction

The increasing use of computers in our society has made us more reliant on computer systems, both hardware and software. The consequence of errors or faults can be severe, causing significant losses, and even damage to property, and injury or death to humans. If we are going to use computers for critical applications, it is important that we know how to design and build systems that we can depend upon.

The major emphasis of this topic will be case studies that examine formal techniques for ensuring highly reliable systems. We'll be focussing on formal hardware verification, both the theory and practice. Part of the course will include practical work.

One week of the course will concentrate on automatic theorem proving.

If there is time we may also examine the use of formal methods in protocol design and verification.

By the end of the topic you should be able to:

• Evaluate the use of selected formal methods;
• Describe the theory of trajectory evaluation and prove its basic theory;
• Apply trajectory evaluation for circuit verification;
• Design simple circuits using a variety of hardware description languages and implement them using field programmable gate arrays;
• Design and implement simple verification systems;
• Explain, implement and apply automatic theorem proving techniques;
• Evaluate and use network specification languages.

Application of Hardware Design Techniques

This section will explore the use of symbolic trajectory evaluation as a verification technique for the design of programmable logic. The material covered includes: symbolic trajectory evaluation and the VossProver verification system; introduction to circuit design and some hardware description languages (Voss EXE, Abel, VHDL); introduction to programmable logic, and in particular field programmable gate arrays (FPGAs).

The section will be evaluated by a case studies and an associated papers. Example: A problem will be selected, and a circuit must be designed to solve the problem. The design must be verified using symbolic trajectory evaluation, and then implemented on an FPGA. For such a case study, a paper must be submitted including:

• description of the problem
• the design of the circuit
• a description of the verification
• a description of the implementation

An evaluation of STE as a verification methodology for programmable logic. The design, proof script and program files (for the FPGA) must also be submitted in computer readable form.

Automatic Theorem Proving

This section of the course will be taught by Dr Peter Jipsen from the Department of Mathematics and Applied Mathematics at the University of This section will first introduce the NPPV tool and then PVS.Cape Town.

General

This course is eight weeks in length. There will be about 25 hours of lectures and labs in total. Students are expected to work a total of 25 hours a week on this course (including lectures and labs). The deadline for the end of the course is fixed because of the commitment of part-time students, so no extensions will be possible.

The major reference for this course is : Thomas Kropf, Formal Hardware Verification: Methods and Systems in Comparison, Springer-Verlag LNCS 1287.


Scott Hazelhurst

About this document ...

Dependable Systems Design Studies

This document was generated using the LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -split 0 -ascii_mode -no_navigation -no_images -no_subdir -show_section_numbers -no_auto_link depend.tex.