Computing Worst Case Execution Time by Symbolically Executing a Time-Accurate Hardware Model
To ensure that a program will respect all its timing constraints the authors must be able to compute a safe estimation of its Worst Case Execution Time (WCET). However, with the increasing sophistication of the processors, computing a precise estimation of the WCET becomes very difficult. In this paper, they propose a novel formal method to compute a precise estimation of the WCET that can be easily parameterized by the hardware architecture. Assuming that there exists an executable timed model of the hardware, they first use symbolic execution to precisely infer the execution time for a given instruction flow. Then, they merge the states relying on the loss of precision they are ready to accept.