The Community for Technology Leaders
RSS Icon
Subscribe
Philadelphia, PA
April 9, 2013 to April 11, 2013
ISBN: 978-1-4799-0186-9
pp: 97-106
B. Blackham , NICTA, Univ. of New South Wales Sydney, Sydney, NSW, Australia
G. Heiser , NICTA, Univ. of New South Wales Sydney, Sydney, NSW, 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 Malardalen 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
Model checking, Semantics, Manuals, Kernel, Real-time systems, Computer architecture, Optimization,Software verification and validation, Real time systems, Operating system kernels
CITATION
B. Blackham, G. 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
41 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool