Formal Specifications of KVM/370 Kernel and Trusted Processes
Abstract
This document contains the formal specification of the kernel and trusted processes of the Kernelized VM operating system (KVM/370). The specification utilizes the specification language INA JO, a proprietary product of System Development Corporation. INA JO is described in TM-6021/000/00, January 1978. This document assumes familiarity with INA JO. The specification is divided into two main parts. Chapter two contains the specification of the kernel, and is split into nineteen sections corresponding to the main areas of functionality of the kernel. For the most part, little or no explanation of the kernel specification is provided; a prose description of each kernel function is contained in 'Preliminary Design of Security Kernel for KVM/370', TM-5855/200/ 00, October 1977. Chapter three contains the specifications of the trusted processes. Each of the five trusted process descriptions has two subsections. The first subsection for each trusted process contains a prose description of the process, detailing its function. The second subsection contains the INA JO specification of the process. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- May 21, 1978
- Accession Number
- ADA109317
Entities
People
- B. D. Gold
- D. H. Thompson
Organizations
- System Development Corporation