An automatic parametric approach for WCET analysis of C programs

International audienceIn this paper, we propose a static worst- case execution time (WCET) analysis approach aimed to automatically extract flow information related to program semantics. This information is used to reduce the overestimation of the calculated WCET. We focus on flow information related to loop bounds and infea- sible paths. The approach handles loops with multiple exit conditions and non-rectangular loops in which the number of iterations of an inner loop depends on the current iteration of an outer loop. The WCET of loops is analytically computed and expressed as summations function of the loop bounds. This avoids unfolding loops while providing tight and safe WCET estimate. Furthermore, the provided WCET expressions are expressed symbolically function of the program input parameters. This allows to reduce the WCET computing cost while providing tight WCET values. In- deed the WCET of each piece of code is expressed assymbolic expression which is instantiated each time that piece is called in the program. The flow analysis uses an enhanced symbolic execution approach based on symbolic execution and an analytic methodin order to avoid unfolding loops performed by symbolic execution-based approaches