PLEA: Parametric loop bound estimation in WCET analysis

Worst-case execution time (WCET) analysis of a program is important to verify the temporal correctness of real-time systems. Parametric WCET analysis represents the WCET of the program as a formula, where the unknown values affecting the WCET are parameterized. Many issues usually affect the WCET of a program, including the loop bound. In parametric timing analysis, instead of determining a constant upper bound for a loop, a symbolic formula represents the loop bound. In this paper, a new method is presented for the parametric loop bound analysis based on path analysis. Instead of considering the basic bocks on their own and independent of the rest, the execution paths within the loop body have to be analyzed. There are certain situations in which the execution of certain statements of an execution path affects the number of executions of all the basic blocks along the execution path. Therefore, more accurate estimation of the number of loop iterations is provided. The results of analysis on the Malardalen benchmark suite reveal the accuracy of the proposed method.