A safety kernel for traffic light control

Author

Ammann, Paul

Author_Institution

Mason Univ., Fairfax, VA, USA

Volume

11

Issue

2

fYear

1996

fDate

2/1/1996 12:00:00 AM

Firstpage

13

Lastpage

19

Abstract

The success of kernels for enforcing security in software systems 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

Keywords

Ada; formal specification; formal verification; operating system kernels; road traffic; safety-critical software; traffic control; traffic engineering computing; Ada implementation; Rushby kernel; feasibility demonstration; formal methods; precise specification; safety kernel; safety-critical applications; scalability; software systems; traffic light control; verification problem; Application software; Costs; Inductors; Kernel; Lighting control; Security; Software maintenance; Software safety; Software systems; Systems engineering and theory;

fLanguage

English

Journal_Title

Aerospace and Electronic Systems Magazine, IEEE

Publisher

ieee

ISSN

0885-8985

Type

jour

DOI

10.1109/62.484300

Filename

484300