CSDL Home R RTAS 2013 2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS)
April 9, 2013 to April 11, 2013
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.
Software verification and validation, Real time systems, Operating system kernels
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