Talks and Poster Presentations (with Proceedings-Entry):

J. Knoop, L. Kovacs, J. Zwirchmayr:
"An Evaluation of WCET Analysis using Symbolic Loop Bounds (extended Abstract)";
Talk: MEMICS 2011 (Mathematical and Engineering Methods in Computer Science), My Hotel, Lednice, Czech Republic; 2011-10-14 - 2011-10-16; in: "MEMICS Proceedings", (2011), 119.

English abstract:
Extended Abstract. The spread of safety critical real time systems results in an in-
creased necessity for worst case execution time (WCET) analysis of these systems:
finding the time limit within which the software system responds in all possible sce-
narios. Computing the WCET for programs with loops or recursion is, in general, un-
decidable. We present an automatic method for computing tight upper bounds on the
iteration number of special classes of program loops. These upper bounds are further
used in the WCET analysis of programs. The technique deploys pattern-based recur-
rence solving in conjunction with program flow refinement using SMT reasoning. To
do so, we refine program flows using SMT reasoning and rewrite certain multi-path
loops into single-path ones, possibly over-approximating the loop-bound. The multi-
path loops we consider are I) abruptly-terminating loops that might terminate early due
to break statements and II) loops with additional monotonic updates, that condition-
ally modify the loop counter. For those, the minimum increase of the loop counter is
computed and used as loop step expression. Single-path loops are further translated into
a set of recurrence relations over program variables. For solving recurrences we deploy
a pattern-based recurrence solving algorithm, computing closed forms for a restricted
class of recurrence equations. Finally, iteration bounds are derived for program loops
from the computed closed forms. We only compute closed forms for a restricted class
of loops, however, in practice, these recurrences describe the behavior of a large set of
program loops that are relevant to WCET analysis. Our technique is implemented in
the r-TuBound tool and was successfully tried out on a number of challenging WCET
benchmarks: we evaluate the symbolic loop bound generation technique and present an
experimental evaluation of the method carried out with the r-TuBound software tool.
We evaluate our method against various academic and industrial WCET benchmarks,
and compare the results to the original TuBound tool.

Electronic version of the publication:

Created from the Publication Database of the Vienna University of Technology.