Fully-automatic derivation of exact program-flow constraints for a tighter worst-case execution-time analysis

Obtaining tight worst-case execution-time (WCET) estimations of real-time tasks is crucial since overly-pessimistic estimations are deemed impractical. One way of making WCET estimations tighter is to incorporate more program-flow information e.g., context-sensitive loop bounds, infeasible-path and same-path information, etc. In this paper we present and evaluate a completely automatic analysis that dynamically derives program-flow information to use in WCET analysis. Flow information is derived by a combination of test-data generation and parsing of program-execution traces to obtain flow-fact hypotheses which are then fed to a model checker to establish their correctness. Experimental evaluation shows that our method help achieve considerable tightness in WCET estimations at a manageable cost.