[Back]

J. Knoop, L. Kovacs, J. Zwirchmayr:
"WCET Squeezing: On-demand Feasibility Refinement for Proven Precise WCET-bounds";
in: "21st International Conference on Real-Time Networks and Systems", Acm Dl, 2013.

The Worst-Case Execution Time (WCET) computed by a WCET
analyzer is usually not tight, leaving a gap between the actual and
the computed WCET of a program. In this article we present a
novel on-demand WCET feasibility refinement technique, called
WCET Squeezing, for minimizing this gap.
WCET Squeezing provides conceptually new means for address-
ing the classical problem of WCET computation, by deriving a
WCET bound that comes as close as possible to the actual one.
WCET Squeezing is an anytime algorithm, that is, it can be stopped
at any time without violating the soundness of its results. This
anytime property allows to apply WCET Squeezing not only for
deriving precise WCET bounds but to also prove additional tim-
ing constraints over the program. Namely, WCET Squeezing can
be used to guarantee that a program is fast enough by ensuring
that the WCET of the program is below some required limit. If
the initially computed WCET of the program is above this limit,
WCET Squeezing can be stopped as soon as the squeezed WCET
of the program is below the limit (proving the program meets the
required timing constraint), or if the squeezed WCET is tight but
above the given limit (proving the program cannot meet the timing
constraint). WCET Squeezing can also be used until a given time
budget is exhausted to compute a tight(er) WCET bound for a pro-
gram. These new applications of WCET Squeezing are out of the
scope of traditional WCET analyzers.
WCET Squeezing combines symbolic program execution with
the Implicit Path Enumeration Technique (IPET) for computing a
precise WCET bound. WCET Squeezing is applicable as a post-
process to any WCET analyzer which encodes the IPET problem
as an Integer Linear Program (ILP). We implemented our method
in the r-TuBound toolchain and evaluated our implementation on a
set examples taken from the Mälardalen WCET benchmark suite.
Our experiments demonstrate that WCET Squeezing can signifi-
cantly tighten the WCET bounds of programs. Moreover, the de-
rived WCET bounds are proven to be precise at a moderate compu-
tational cost.

WCET analysis, Refinement, Symbolic Execution, Real-time systems, Embedded Systems

http://publik.tuwien.ac.at/files/PubDat_221282.pdf