DocumentCode
3348000
Title
A small real-time kernel proven correct
Author
Tol, Ronald M.
Author_Institution
Dept. of Comput. Sci., Groningen Univ., Netherlands
fYear
1992
fDate
2-4 Dec 1992
Firstpage
227
Lastpage
230
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Systems Symposium, 1992
Conference_Location
Phoenix, AZ
Print_ISBN
0-8186-3195-3
Type
conf
DOI
10.1109/REAL.1992.242659
Filename
242659
Link To Document