Title :
Extended abstract: evaluation of delay queues for a Ravenscar HW kernel
Author :
Naeser, Gustaf ; Furunäs, Johan
Author_Institution :
Dept. of Comput. Sci. & Electron., Malardalen Univ., Sweden
Abstract :
This extended abstract presents work in progress on the evaluation of four delay queues designed for application tailored Ravenscar hardware real-time kernels. The properties of the different queues and optimizations of them are discussed, both for the formal models and for the actual hardware implementations of the queues. Our study of the queues shows that even though parallelism costs much in terms of chip area, there are system configurations where it is the most space conservative.
Keywords :
formal specification; formal verification; operating system kernels; parallel processing; queueing theory; real-time systems; Ravenscar hardware real-time kernel; delay queue; formal specification; formal verification; operating system kernels; parallelism; Application software; Clocks; Computer science; Delay effects; Dynamic programming; Hardware; Kernel; Queueing analysis; Real time systems; Timing;
Conference_Titel :
Formal Methods and Models for Co-Design, 2005. MEMOCODE '05. Proceedings. Third ACM and IEEE International Conference on
Print_ISBN :
0-7803-9227-2
DOI :
10.1109/MEMCOD.2005.1487926