On attaining reliable software for a secure operating system

This paper presents a general methodology for the design, implementation, and proof of large software systems, each described as a hierarchy of abstract machines. The design and implementation occur in five stages as described in this paper. Formal proof may take place at each stage. We expect the methodology to simplify the proof effort in such a way as to make proof a feasible tool in the development of reliable software. In addition to the anticipated advantages in proof, we feel that the methodology improves a designer's ability to formulate and organize the issues involved in the design of large systems, with additional benefits in system reliability. These advantages remain even if proof is not attempted.