Item Details

Print View

A Safety Kernel Architecture

Wika, Kevin; Knight, John
Wika, Kevin
Knight, John
Software plays a crucial role in a large number of safety-critical systems. In spite of this, many safety-critical systems exhibit residual software errors even after extensive implementation and verification efforts. We describe a software architecture based on a safety kernel that facilitates the implementation and verification of safety-critical software. Drawing many concepts from the related notion of a security kernel, the safety kernel enforces safety policies independent of application programs and permits verification of properties of a small kernel rather than large amounts of application software. Safety-critical software is typically custom-built for each application. This leads to consistently high development costs and limited reuse of either designs or software modules. We believe that the safety kernel architecture provides a framework for identification of generally applicable classes of safety policies. The paper examines several classes of kernel-enforced policies. The policies have been identified using criteria that consider the criticality of a policy and the effects of kernel enforcement on the simplicity and verifiability of both the application software and the safety kernel. These general policies are parameterized to enable configuration of an instance of the safety kernel. A mechanical translator is utilized to instantiate the safety kernel from the parameter information. The concepts and design of the safety kernel architecture have been significantly influenced by our research into the development of dependable software for an experimental neurosurgical device. For example, having worked with this "real" system, we recognized that in general the safety kernel would need to coexist with a large amount of potentially unreliable software. As a result, we describe a system architecture wherein the safety kernel operates in the context of application and system software that is unreliable or at least of unknown properties. Note: Abstract extracted from PDF text
Date Received
University of Virginia, Department of Computer Science, 1994
Published Date
Libra Open Repository
In CopyrightIn Copyright
▾See more
▴See less


Access Online