An automatic parametric approach for WCET analysis of C programs

Djemaï Kebbal (1)

1 IRIT - Institut de recherche en informatique de Toulouse

In 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 as symbolic 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 method in order to avoid unfolding loops performed by symbolic execution-based approaches.

Mots clés: automatic parametric flow analysis; block-based symbolic execution; symbolic expression simplification

Domaines: Informatique [cs]; Systèmes embarqués

Djemaï Kebbal. An automatic parametric approach for WCET analysis of C programs. ERTS2 2010, Embedded Real Time Software & Systems, May 2010, Toulouse, France. ⟨hal-02267655⟩