# Worst-case execution-time analysis

Worst-case execution-time (WCET) analysis computes an upper bound on a
task's running time, *guaranteed* by construction rather than measured.
In a hard-real-time system (a flight controller, an airbag trigger, an
engine controller), a task that misses its deadline has failed as surely
as one that computes the wrong answer, and showing the schedule is
feasible needs exactly that bound.

That guarantee makes it a formal method, sibling to
[abstract interpretation](https://quality.stereobooster.com/abstract-interpretation.md) and
[termination analysis](https://quality.stereobooster.com/termination-analysis.md): a sound static
analysis that *proves* a property rather than measuring it. What
separates it from
the measured performance methods ([profiling](https://quality.stereobooster.com/profiling.md)
and [load testing](https://quality.stereobooster.com/load-and-stress-testing.md)) is the
guarantee: they report typical, measured time; WCET bounds the
*worst* case, soundly.

## What it establishes

- **A guaranteed ceiling on execution time** for a task or path,
  never an underestimate: an optimistic bound that a real run can
  exceed is unsafe in a hard-real-time schedule.
- **An input to schedulability analysis.** Given a sound bound per
  task, a scheduling analysis can prove the whole task set meets its
  deadlines.

The bound is only as sound as the hardware
model: an effect the model omits (speculative execution, a cache
level, memory-refresh timing, multicore bus contention) either breaks
soundness or forces a looser, more pessimistic bound.

## How it works

Sound static WCET works in two layers:

- **Micro-architectural analysis** models the processor (caches,
  pipeline, branch prediction) to bound the time of each basic block,
  using [abstract interpretation](https://quality.stereobooster.com/abstract-interpretation.md) over the
  cache and pipeline states. Deep pipelines and multi-level caches
  multiply the processor states the analysis must track, so it
  abstracts them more coarsely and the bound it proves sits further
  above the real worst case. Multicore bus contention pushes the bound
  further still.
- **Path analysis** then finds the longest feasible path through the
  program given those per-block bounds. The implicit path enumeration
  technique (IPET) encodes the control-flow graph and loop bounds as an
  integer linear program (ILP) and maximizes total time. Loop bounds
  must be known (annotated or inferred), since an unbounded loop has no
  finite WCET.

**Measurement-based WCET** instead runs the code on the target and
takes the maximum observed time plus a safety margin. It is far
easier and needs no hardware model, but it is not sound: the harness
may never hit the worst-case path or cache state. Hybrid methods
measure basic blocks and combine them along the IPET path.

## Tools

- **aiT** (AbsInt, commercial) — a sound WCET analyzer, shipped with a
  vendor qualification kit for DO-178C avionics certification.
- **[OTAWA](https://gitlab.com/otawa)** and **[Heptane](https://team.inria.fr/pacap/software/heptane/)** — open-source
  academic WCET frameworks, used in research and teaching.
- Measurement-based and hybrid tools (RapiTime, from Rapita Systems, is
  commercial) trade the soundness guarantee for applicability to
  complex processors.

## When to use, when not

**Use** it for hard real-time and safety-critical software where a
missed deadline is catastrophic and the schedule must be *proved*
feasible: avionics, automotive, aerospace, industrial control, under
regimes like DO-178C.

**Don't** reach for it for soft real-time or general software, where a
late response degrades rather than endangers: profiling and load
testing give the typical-time picture that case needs, far more
cheaply. Sound WCET is also most tractable on the simpler, predictable
processors of embedded systems; on commodity out-of-order, speculative
CPUs a tight sound bound is often impractical.

## Evidence

The guarantee is definitional: a sound WCET analysis returns an upper
bound that is correct by construction for the hardware model it
assumes. How *tight* that bound is does not follow from the guarantee,
and the true worst case it would be compared against is itself unknown
— a run is not guaranteed to hit the worst-case path or cache state.

## Further reading

- The methods and the tool landscape are cataloged in the standard
  survey by Wilhelm and colleagues (Wilhelm et al. 2008)[^wilhelm2008].

## Related

**Bounding a program's cost**

All three ask how much a computation costs, and meet the same undecidable core (the
halting problem) at different guarantee levels. [Termination
analysis](https://quality.stereobooster.com/termination-analysis.md) proves the qualitative floor: does
the program halt at all, over every input. Worst-case execution-time
analysis assumes it halts and proves a sound *upper*
bound on running time for the modeled hardware. [Algorithmic complexity
testing](https://quality.stereobooster.com/algorithmic-complexity.md) trades proof for search: it hunts an
input that drives cost past its expected growth, witnessing a *lower* bound on how bad
the worst case gets.

Termination is the precondition, since a runtime that might be infinite has no bound to
compute. WCET and complexity testing then bracket the same worst case from opposite
sides: WCET over-approximates (sound, never optimistic, sometimes pessimistic), while
complexity testing under-approximates (a blow-up it finds is real, but finding none
proves nothing). The two sound static methods and the one empirical search are the
formal and the testing answers to a single question about resource use.

## Classification

- **Quality dimensions:** Performance, Functionality: safety.
- **Area:** Hard-real-time and safety-critical embedded software — avionics, automotive, aerospace, industrial control — where a task must provably finish within its deadline.
- **Guarantee:** Exhaustive — a sound upper bound, guaranteed to be at least any actual execution time, for the modeled hardware.

## Referenced by

- [Formal methods](https://quality.stereobooster.com/formal.md) · Methods
- [Verifying safety-critical systems](https://quality.stereobooster.com/safety.md) · Methods

## References

[^wilhelm2008]: Wilhelm, Reinhard, Jakob Engblom, Andreas Ermedahl, et al. 2008. "[The Worst-Case Execution-Time Problem — Overview of Methods and Survey of Tools](https://www.es.mdh.se/pdf_publications/1258.pdf)." *ACM Transactions on Embedded Computing Systems* 7 (3): 1–53. <https://doi.org/10.1145/1347375.1347389>.

## Acronyms

- ILP — integer linear programming
- IPET — implicit path enumeration technique
- WCET — worst-case execution time