A small real-time kernel proven correct
- 2 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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
This publication has 3 references indexed in Scilit:
- Constructing Predictable Real Time SystemsPublished by Springer Nature ,1991
- Feasible processor allocation in a Hard-Real-Time environmentReal-Time Systems, 1989
- Scheduling Algorithms for Multiprogramming in a Hard-Real-Time EnvironmentJournal of the ACM, 1973