Lawrence Flon

On the Design and Verification of Operating Systems Degree Type: Ph.D. in Computer Science
Advisor(s): Nico Habermann
Graduated: August 1977

Abstract:

This thesis applies and extends mathematical program verification to systems programs. The design methodology is based upon the use of abstract data types and the construction and verification of both specifications and implementations for them. The abstract data type is a means of modularization which encapsulates the representation of a data structure and the algorithms which operate directly upon it. The specification technique appeals to various mathematical structures e.g. sets and sequences to describe an abstract state for objects of a given type. The correctness of the formal specifications is cast in terms of the proof of certain invariant properties of the abstract state.

An axiomatic proof rule is given to formulate the theorems necessary for proving the invariance of predicates across formal specifications. The applicability of the methodology to operating systems is explored. It is found that a hierarchical decomposition is most amenable to verification, and that the implementation language used is a function of that hierarchy. The example of a process dispatcher module of a hypothetical operating system is used to illustrate the process of design, specification, implementation, and verification using the methodology. Various properties are proven of the abstract specifications, including one representation of the concept of fair service. Programs are then written for the specifications and their correctness is verified.

Thesis Committee:
Nico Habermann (Chair)

Joseph Traub, Head, Computer Science Department