WCET: SEmantics, Precision, Traceability – W-SEPT

The design flow of critical applications shows 3 levels of description: high level models (Matlab/Simulink,
Scade), intermediate code (C), and finally binanry code. Discovering functional properties becomes harder as the
level get close to the machine. The approach of the project is to discover, transmit and exploit functionnal
information all along the design flow.

The main result is a better exploitation of the functional aspects in the WCET estimations. The approch is validated by the development of proof-of-concept tools and methods, with a special attention to the integration into the methods actually used in the industry. In particular, the results will be made available to the academic and industrial community though their integration into the open-source tool-box OTAWA.

The project falls in the general goal of developing and promoting static temporal analysis techniques. Conversely
to measurement-based empirical techniques, this kind of analysis gives guaranteed upper-approximations, which is
dramatically important in critical domains (e.g. avionics), that are subject to certification constraints.

The project has been presented during the kick-off of the Timing Analysis on Code-Level action (TACLe), from the
European network COST, and in the workshop Synchron (http://synchron2012.inria.fr/). Ongoing publications are
planned on the main conferences of the domain.

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.

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 properties 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 information 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
semantic 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 dedicated
to WCET analysis (Otawa) and experimented on several case studies from
the spatial and automotive domains.