Computing Worst Case Execution Time by Symbolically Executing a Time-accurate Hardware Model

To ensure that a program will respect all its timing constraints we 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, we 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, we first use symbolic execution to precisely infer the execution time for a given instruction flow.Then we merge the states relying on the loss of precision we are ready to accept.