DocumentCode
2973693
Title
Formal development of a real-time kernel
Author
Fowler, Simon ; Wellings, Andy
Author_Institution
Dept. of Comput. Sci., York Univ., UK
fYear
1997
fDate
5-5 Dec. 1997
Firstpage
220
Lastpage
229
Abstract
The formal development of a simple real time operating system kernel is described. The kernel provides a set of operations that allows a restricted Ada 95 tasking model to be supported, suitable for fixed priority real time systems. The requirements for the kernel are expressed in terms of the computational model using RTL, and the abstract specification of the kernel is validated against this. The development of an implementation from this specification is then described, with the PVS proof system used to verify each step in the development process.
Keywords
Ada; formal specification; operating system kernels; real-time systems; theorem proving; PVS proof system; RTL; abstract specification; computational model; fixed priority real time systems; formal development; restricted Ada 95 tasking model; simple real time operating system kernel; Asynchronous communication; Computational modeling; Computer science; Concurrent computing; Delay; Kernel; Logic; Operating systems; Protection; Real time systems;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Systems Symposium, 1997. Proceedings., The 18th IEEE
Conference_Location
San Francisco, CA, USA
ISSN
1052-8725
Print_ISBN
0-8186-6600-5
Type
conf
DOI
10.1109/REAL.1997.641284
Filename
641284
Link To Document