[PostDoc] Enhancing WCET Estimation by Exploiting Program Semantics

supervisors: Claire Maiza, Pascal Raymond

Postdoctoral researcher (6 to 18 months)

Scientific context:

Critical embedded systems are generally composed of repetitive tasks that must meet drastic timing constraints, such as termination deadlines. Providing an upper bound of the worst-case execution time (WCET) of such tasks at design time is thus necessary to prove the correctness of the system. Dynamic methods based on testing give realistic but unsafe results: they are not guaranteed to pinpoint the worst-case execution. On the contrary, static timing analysis methods, compute safe WCET upper bounds, but at the cost of a potentially large over-approximation. Sources of over-estimation stem from the analysis of the hardware platform, but also from the unfeasible executions due to the semantics of the program itself.

Much effort has been devoted to model the hardware precisely. In comparison, handling semantic aspects in timing analysis has been less studied. It has been mainly limited to the estimation of loop bounds and rather simple infeasible paths. In addition, the scope of semantic properties that can be expressed and exploited with the most widely used resolution method (IPET: Implicit Paths Enumeration Technique) has not been clearly established yet.

Objectives of the Post-Doc

The purpose of this position is precisely to study these points: how (useful) semantic information on feasible paths can be represented and exploited in the WCET analysis. A first idea is to study the class of information that can be expressed within the existing state-of-the-art IPET framework. This work should naturally lead to a survey on alternative methods, possibly more suitable to exploit semantic information.

Terms of employment

A full-time position as a postdoctoral researcher for a period of 6 to 18 months starting as soon as possible. The position will be funded by the ANR/INS project W-SEPT. The salary will be 2500 EUR gross per month depending on qualifications and experience.

Application

Send a detailed CV, a list of publications, a list of referees (persons that can recommend you), and a short letter explaining your motivations for this position, by email to:

Claire.Maiza@imag.fr, Pascal.Raymond@imag.fr

Please include [POSTDOC W-SEPT] in the subject of your mail, and only attach PDF files.