Please use this identifier to cite or link to this item: https://doi.org/10.1109/RTSS.2011.38
DC FieldValue
dc.titleTiming analysis of a protected operating system kernel
dc.contributor.authorBlackham, B.
dc.contributor.authorShi, Y.
dc.contributor.authorChattopadhyay, S.
dc.contributor.authorRoychoudhury, A.
dc.contributor.authorHeiser, G.
dc.date.accessioned2013-07-04T08:43:15Z
dc.date.available2013-07-04T08:43:15Z
dc.date.issued2011
dc.identifier.citationBlackham, B.,Shi, Y.,Chattopadhyay, S.,Roychoudhury, A.,Heiser, G. (2011). Timing analysis of a protected operating system kernel. Proceedings - Real-Time Systems Symposium : 339-348. ScholarBank@NUS Repository. <a href="https://doi.org/10.1109/RTSS.2011.38" target="_blank">https://doi.org/10.1109/RTSS.2011.38</a>
dc.identifier.isbn9780769545912
dc.identifier.issn10528725
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/42096
dc.description.abstractOperating 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 thirdgeneration microkernel. seL4 is the world's first formallyverified 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 timesharing 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 microkernels, and properties of seL4's source code arising from the requirements of formal verification. © 2011 IEEE.
dc.description.urihttp://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1109/RTSS.2011.38
dc.sourceScopus
dc.subjectOperating system kernels
dc.subjectReal time systems
dc.subjectSoftware verification and validation
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.doi10.1109/RTSS.2011.38
dc.description.sourcetitleProceedings - Real-Time Systems Symposium
dc.description.page339-348
dc.description.codenPRSYE
dc.identifier.isiutNOT_IN_WOS
Appears in Collections:Staff Publications

Show simple item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

40
checked on Nov 20, 2019

Page view(s)

129
checked on Oct 28, 2019

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.