Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis

Select |




Print


Sewell, Thomas; Kam, Felix; Heiser, Gernot

Sewell, Thomas; Kam, Felix; Heiser, Gernot


2016-04-11


Conference Material


IEEE Real-Time and Embedded Technology and Applications Symposium


Vienna, Austria


11


Worst-case execution time (WCET) analysis of real-time code needs to be performed on the executable binary code for soundness. Determination of loop bounds and elimination of infeasible paths, essential for obtaining tight bounds, frequently depends on program state that is difficult to extract from static analysis of the binary. Obtaining this information generally requires manual intervention, or compiler modifications to preserve more semantic information from the source program. We propose an alternative approach, which leverages an existing translation-validation framework, to enable high-assurance, automatic determination of loop bounds and infeasible path. We show that this approach automatically determines all loop bounds as well as many (possibly all) infeasible paths in the seL4 microkernel, as well as in standard WCET benchmarks which are in the language subset of our C parser.


WCET, seL4, real-time, translation validation


http://2016.rtas.org/


nicta:9118


Sewell, Thomas; Kam, Felix; Heiser, Gernot. Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis. In: IEEE Real-Time and Embedded Technology and Applications Symposium; Vienna, Austria. 2016-04-11.



Loading citation data...

Citation counts
(Requires subscription to view)