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

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