  Estimating the Worst-Case Execution Time (WCET) of an application is an
essential task in the context of developing real-time or safety-critical
software, but it is also a complex and error-prone process. Conventional
approaches require at least some manual inputs from the user, such as loop
bounds and infeasible path information, which are hard to obtain and can lead
to unsafe results if they are incorrect. This is aggravated by the lack of a
comprehensive explanation of the WCET estimate, i.e., a specific trace showing
how WCET was reached. It is therefore hard to spot incorrect inputs and hard to
improve the worst-case timing of the application. Meanwhile, modern processors
have reached a complexity that refutes analysis and puts more and more burden
on the practitioner. In this article we show how all of these issues can be
significantly mitigated or even solved, if we use processors that are amenable
to WCET analysis. We define and identify such processors, and then we propose
an automated tool set which estimates a precise WCET without unsafe manual
inputs, and also reconstructs a maximum-detail view of the WCET path that can
be examined in a debugger environment. Our approach is based on Model Checking,
which however is known to scale badly with growing application size. We address
this issue by shifting the analysis to source code level, where source code
transformations can be applied that retain the timing behavior, but reduce the
complexity. Our experiments show that fast and precise estimates can be
achieved with Model Checking, that its scalability can even exceed current
approaches, and that new opportunities arise in the context of "timing
debugging".
