Nos partenaires



Accueil du site > Français > Evénements > Séminaires



L’IRIT étant localisé sur plusieurs sites, ses séminaires sont organisés et ont lieu soit à l’Université Toulouse 3 Paul Sabatier (UT3), l’Université Toulouse 1 Capitole (UT1), l’INP-ENSEEIHT ou l’Université Toulouse 2 Jean Jaurès (UT2J).


Symbolic Methods for the Timing Analysis of Programs

Jakob ZWIRCHMAYR - Equipe TRACES - IRIT (France)

Lundi 27 Janvier 2014, 10h00
UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
Version PDF :


An important property of embedded safety-critical real-time systems is the Worst-Case Execution Time (WCET) of the system: the maximal running time of the program on the specified hardware. Often, due to the employed abstractions, the WCET is actually computed for a spuri- ous trace in the program, giving no hint whether the bound is precise or whether it is an over-estimation of a spurious system execution. In this talk we present a method for proving WCET bounds precise. It guaran- tees that the WCET bound is actually computed for a feasible trace in the system. Moreover, our method is able to improve the WCET analysis quality by reducing the required manual annotations and the imprecision of WCET estimates, automatically tightening the WCET bound until precise when necessary by means of symbolic execution. In order to overcome the computationally expensive costs of symbolic execution, our challenge is to identify and apply it only on relevant program parts. This way, the precision of symbolic execution is exploited while avoiding the computational costs.