The Community for Technology Leaders
RSS Icon
Subscribe
Philadelphia, PA, USA USA
Apr. 9, 2013 to Apr. 11, 2013
ISBN: 978-1-4799-0186-9
pp: 97-106
Bernard Blackham , NICTA and University of New South Wales Sydney, Australia
Gernot Heiser , NICTA and University of New South Wales Sydney, Australia
ABSTRACT
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, 2013, 2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS), 2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS) 2013, pp. 97-106, doi:10.1109/RTAS.2013.6531083
27 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool