Paper Info
Title
Timing Analysis of a Protected Operating System Kernel
Abstract
Operating systems offering virtual memory and protected address spaces have been an elusive target of static worst-case execution time (WCET) analysis. This is due to a combination of size, unstructured code and tight coupling with hardware. As a result, hard real-time systems are usually developed without memory protection, perhaps utilizing a lightweight real-time executive to provide OS abstractions. This paper presents a WCET analysis of seL4, a third-generation micro kernel. seL4 is the world's first formally-verified operating-system kernel, featuring machine-checked correctness proofs of its complete functionality. This makes seL4 an ideal platform for security-critical systems. Adding temporal guarantees makes seL4 also a compelling platform for safety- and timing-critical systems. It creates a foundation for integrating hard real-time systems with less critical time-sharing components on the same processor, supporting enhanced functionality while keeping hardware and development costs low. We believe this is one of the largest code bases on which a fully context-aware WCET analysis has been performed. This analysis is made possible due to the minimalistic nature of modern micro kernels, and properties of seL4's source code arising from the requirements of formal verification.
Year
DOI
Venue
2011
10.1109/RTSS.2011.38
RTSS
Keywords
Field
DocType
third-generation microkernel,protected operating,operating system kernel protection,enhanced functionality,software verification and validation,complete functionality,os abstractions,protected address spaces,wcet analysis,operating system kernels,system kernel,context-aware wcet analysis,static worst-case execution time analysis,virtual memory,compelling platform,lightweight real-time executive,sel4,security-critical systems,source coding,real time systems,largest code base,unstructured code,memory protection,hard real-time systems,hard real-time system,safety-critical software,source code,machine-checked correctness proofs,timing analysis,timing-critical systems,real-time systems,formal verification,security of data,worst case execution time,time sharing,operating system,real time,tight coupling,software verification
Kernel (linear algebra),Memory protection,Source code,Computer science,Virtual memory,Real-time computing,Static timing analysis,Software verification and validation,Coupling (computer programming),Formal verification,Distributed computing,Embedded system
Conference
ISSN
ISBN
Citations 
1052-8725
978-1-4577-2000-0
33
PageRank 
References 
Authors
1.11
12
5
Name
Order
Citations
PageRank
Bernard Blackham1694.41
Yao Shi212413.96
Sudipta Chattopadhyay327721.09
Abhik Roychoudhury42449122.18
Gernot Heiser52525137.42