A Verified Specification of a Hierarchical Operating System.

摘要

This thesis discusses the design, specification, and verification of computer operating systems. The operating system problem considered, the many process problem, is the design of an operating system that can support a large number of concurrent processes. This design problem is a vehicle to investigate the use of a design methodology, the hierarchical levels of abstraction methodology; the use of structured programming techniques in the specification of the system; and the development of techniques for the verification of concurrent programs, particularly operating system programs. A solution to the many-process problem is obtained and it is shown that the hierarchical levels of abstraction methodology simplifies the conception of the solution and helps avoid potential deadlocks in the system. A PASCAL specification of the four levels of the system is given demonstrating the usefulness of structured programming techniques for specifying operating system programs.