Computing worst case execution time (WCET) by Symbolically Executing a time-accurate Hardware Model

Abstract—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 [1] 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.