BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Real-Time and Real Trustworthiness: Timing Analysis of a Protected
  OS Kernel - Bernard Blackham (NICTA)
DTSTART:20111121T150000Z
DTEND:20111121T160000Z
UID:TALK34659@talks.cam.ac.uk
CONTACT:Eiko Yoneki
DESCRIPTION:Protected operating systems have been an elusive target of sta
 tic worst-case execution time (WCET) analysis\, due to a combination of th
 eir size\, unstructured code and tight coupling with hardware. As a result
 \, critical hard real-time systems are usually developed without memory pr
 otection\, in order to provide guarantees on their response time.\n\nIn th
 is talk\, I will explore a WCET analysis of seL4\, a third-generation micr
 okernel. seL4 is the world’s first formally-verified operating-system ke
 rnel\, featuring machine-checked correctness proofs of its complete functi
 onality. This makes seL4 an ideal platform for security-critical systems. 
 Adding temporal guarantees makes seL4 also a compelling platform for safet
 y- and timing-critical systems. It enables hard real-time systems with les
 s critical time-sharing components to be integrated on the same processor\
 , supporting enhanced functionality while keeping hardware and development
  costs low.\n\nThe talk will focus on the more interesting aspects of the 
 analysis\, and in particular\, properties of the seL4 code base which made
  life easier in the process.\n\nThis work was presented at: Real-time Syst
 ems Symposium 2011 (Vienna\, Austria)\n\nBio: Bernard is a PhD candidate a
 t the University of New South Wales and NICTA in Sydney\, Australia. His P
 hD relates to real-time aspects of the seL4 microkernel. Bernard's researc
 h interests include static analysis\, process checkpointing\, and generall
 y messing with anything executable. Bernard also trains the Australian tea
 m for the International Olympiad in Informatics.\n\n
LOCATION:FW26\, Computer Laboratory\, William Gates Builiding
END:VEVENT
END:VCALENDAR