Introduction
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 never guaranteed to pinpoint the worst-case execution. On the contrary, static timing analysis methods, considered in the project, compute safe WCET upper bounds, but at the cost of a potentially large over-approximation. Their results are often considered too pessimistic and unrealistic to be used by most industrial sectors. Sources of over-estimation stem from the analysis of the hardware platform, but also from the identification of semantic information in programs to detect feasible executions. 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 determining 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.
Objectifs
The key position of this proposal is to bring semantics back to the heart of timing analysis. The final goal is a gain in precision of the WCET estimate. It will be reached by introducing new strategies at different levels in the whole analysis process. First of all, the semantic proper- ties that are relevant and useful for enhancing timing analysis will be characterized. Semantic information can be discovered from high-level design (when it exists, e.g. Scade, Simulink), from the C code, and/or from the binary code. Solutions to ensure the traceability of the in- formation though the compilation process will be proposed. Then, the state-of-the-art WCET computation method (IPET) will be re-visited to investigate to what extent it can exploit the se- mantic information transferred from previous steps. Alternative methods will be proposed to go beyond its limitations. All the contributions will be implemented in an open-source toolset ded- icated to WCET analysis (Otawa) and experimented on several case studies from the spatial and automotive domains.
Partenaires
Personnel VERIMAG impliqué
- Claire Maïza
- Pascal Raymond
- Erwan Jahier
- Nicolas Halbwachs
- Fabienne Carrier
- Catherine Parent
- Mihail Asavoae (Postdoc)
