Item Details

Safety Kernel Enforcement of Software Safety Policies

Wika, Kevin
Format
Report
Author
Wika, Kevin
Abstract
Computing systems in which the consequences of failure are very serious are termed safety - critical. Many such systems exist in application areas such as aerospace, defense, transportation, power-generation, and medicine. The software in these systems is typically large and complex, critical to system safety, and difficult to implement and verify. Even when great effort is expended to develop the software, there is no assurance that the soft» ware will operate with the required level of dependability. We have investigated a safety kernel architecture that addresses part of the problem of building and verifying dependable safety - critical software. An analogous construct, the security kernel, has been used successfully to enforce security policies in - mation systems. Similar requirements known as safety policies must be enforced in safetycritical systems. Other researchers have developed some basic safety kernel concepts and have proposed safety kernel designs. However, many feasibility issues have not been addressed previously. Thus, the focus of this research has been the evaluation and develop -merit of the safety kernel as a software architecture for enforcement of safety policies. We have evaluated the feasibility of the safety kernel in four areas: policy enforcement, reliable enforcement, implementation, and verification. The first area addresses the role of the safety kernel and assesses its support for safety - critical systems. The second, area examines the requirements for reliable policy enforcement by the safety kernel. The third area focuses on the feasibility of a reuse - oriented implementation strategy. The fourth area considers the verification of the safety kernel. Work in each of these areas has been supported by our involvement with two case studies: the Magnetic Stereotaxis System and the University of Virginia Reactor. The results presented in this dissertation demonstrate that it is feasible for the safety kernel to enforce a significant set of safety policies - policies that are directly related to device operation. Fuitheimore, operating in the system context, it can enforce policies reliably in spite of certain component failures. We demonstrate that a special~purpose specifi- cation language can be used to describe the safety kernel and that a source code representation of the safety kernel can be mechanically generated from this policy specifi- cation. Finally, we define the issues in verification of the safety kernel and demonstrate the feasibility of several analysis and testing techniques. Note: Abstract extracted from PDF file via OCR
Language
English
Date Received
20121029
Published
University of Virginia, Department of Computer Science, 1995
Published Date
1995
Collection
Libra Open Repository
Logo for In CopyrightIn Copyright

Availability

Access Online