Correctness in operating systems

Abstract

In a method of program verification introduced by Floyd, assertions are attached to a flowchart description of a program, and correctness is established by showing their consistency with respect to that flowchart. In this thesis, the method has been extended to apply to concurrently executing programs such as those which occur in operation systems. This has required a careful definition of process and an effective representation of the interactions among processes. For this purpose, a flowchart-like representation was chosen to characterize all possible computations resulting from the asynchronous execution of two programs. Floyd's results were then applied to this representation to transform a problem of verifying a set of programs into a problem of proving a theorem of logic. Simplifications suggested by the structure of the programs are applied to reduce the level of difficulty. Transformations suggested by the interactions of the programs are applied to facilitate the effective characterization of properties of interest. (Author)