DTIC ADA040699: A Verified Specification of a Hierarchical Operating System.Reportar como inadecuado




DTIC ADA040699: A Verified Specification of a Hierarchical Operating System. - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Descargar gratis o leer online en formato PDF el libro: DTIC ADA040699: 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 hierarc

Autor: Defense Technical Information Center

Fuente: https://archive.org/


Introducción



SU-SEL-76-011 A VERIFIED SPECIFICATION OF A HIERARCHICAL OPERATING SYSTEM by Ashok R.
Saxena January 1976 Technical Report No.
107 DIGITAL SYSTEMS LABORATORY Department of Electrical Engineering Stanford University Stanford, California L * L r A VERIFIED SPECIFICATION OF A HIERARCHICAL OPERATING SYSTEM by Ashok R.
Saxena Technical Report No.
107 January 1976 Digital Systems Laboratory [ Department of Electrical Engineering Stanford University Stanford, California ABSTRACT This thesis discusses the design, specification, and vertification 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.
A detailed description of the development of the simple memory manager, a complex and large segment of the system, is given to show the use of step-wise refinement for improving the efficiency of the program and as an aid in understanding its final specification.
The specifications for the first two levels; simple scheduler and simple memory manager, are formally verified.
The notion of exclusive access of a resource has been formalized and used in the verification of concurrent program.
Sufficient conditions for verifying the abs...





Documentos relacionados