Abstract

The success of kernels for enforcing security has led to proposals to use kernels for enforcing safety. This paper presents a feasibility demonstration of one particular proposal for a safety kernel via the application of traffic light control. The paper begins with the safety properties for traffic light control and specifies a kernel that maintains the safety properties. An implementation sketch of the kernel in Ada is given and use of the kernel is discussed. The contribution of the paper is a demonstration that a kernel is a feasible and desirable technique for software in a realistic, safety-critical application. The paper also illustrates how formal methods aid the software engineer in constructing and reasoning about such software.

Paper

A complete version of the paper is available in postscript.