Title :
A small real-time kernel proven correct
Author_Institution :
Dept. of Comput. Sci., Groningen Univ., Netherlands
Abstract :
A novel computer architecture for hard real-time environments is being developed. Part of the architecture is an operating system kernel supporting the real-time features of an extended version of the real-time programming language PEARL. The formal verification of a stripped-down version of this real-time kernel using a mechanical theorem prover is presented. Since the author is aiming at a formal verification of the complete kernel, he gives an outline of what still has to be done
Keywords :
computer architecture; formal verification; network operating systems; real-time systems; theorem proving; computer architecture; formal verification; hard real-time environments; operating system kernel; real-time programming language PEARL; small real-time kernel; Application software; Computer architecture; Computer languages; Delay; Formal specifications; Formal verification; Kernel; Operating systems; Real time systems; Timing;
Conference_Titel :
Real-Time Systems Symposium, 1992
Conference_Location :
Phoenix, AZ
Print_ISBN :
0-8186-3195-3
DOI :
10.1109/REAL.1992.242659
