This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS)
Sequoll: A framework for model checking binaries
Philadelphia, PA, USA USA
April 09-April 11
ISBN: 978-1-4799-0186-9
Bernard Blackham, NICTA and University of New South Wales Sydney, Australia
Gernot Heiser, NICTA and University of New South Wales Sydney, Australia
Multi-criticality real-time systems require protected-mode operating systems with bounded interrupt latencies and guaranteed isolation between components. A tight WCET analysis of such systems requires trustworthy information about loop bounds and infeasible paths. We propose sequoll, a framework for employing model checking of binary code to determine loop counts and infeasible paths, as well as validating manual infeasible path annotations which are often error-prone. We show that sequoll automatically determines many of the loop counts in the Ma¨lardalen WCET benchmarks. We also show that sequoll computes loop bounds and validates several infeasible path annotations used to reduce the computed WCET bound of seL4, a high-assurance protected microkernel for multi-criticality systems.
Index Terms:
Software verification and validation,Real time systems,Operating system kernels
Citation:
Bernard Blackham, Gernot Heiser, "Sequoll: A framework for model checking binaries," rtas, pp.97-106, 2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS), 2013
Usage of this product signifies your acceptance of the Terms of Use.