In planes and cars, any failure may lead to injuries for driver orpassengers. For these critical systems, correct operations also means satisfying some temporal constraints(for instance, answering within 50ms). In order to ensure these timing constraints, one must prove thattheir Worst Case Execution Time (WCET) is bounded. Static timing analysis is composed of hardwareand software model to estimate a bound on this WCET. For dynamic behaviour such as out-of-orderexecution, building a static model may lead to accuracy and complexity issues.
The objective of this internship is to develop a processor model to explore a timing issue named timing anomaly. A timing anomaly happens whenever a local worst-case behaviour (a cache miss, for instance) leads to a shorter global execution than the local best case (a cache hit may cost more). This may happen, for instance, in the case of a cache hit, the access is terminated earlier and a time window is free for executing something else in the pipeline that will impact the total execution time.
In this internship the focus will be on the exploration of the timing anomaly impact using a model-checker. Particularly, we aim at a model for a real hardware platform. A model checker is a tool to formally verify properties on a model. The main question is at which level should be the model to stay accurate while keeping the complexity low enough for practical usage. The state of the art covers these topics : WCET analysis, timing anomaly definition and hardware model by model checking. There is two aspects to this internship : the theoretical part with the study of a convenient model, the implementation part in a model-checker.
Expected ability of the student : Automata, logic (to express properties) and hardware notions are mandatory.
J. Eisinger, I. Polian, B. Becker, S. Thesing, R. Wilhelm, and A. Metzner. 2006. Automatic Identification of Timing Anomalies for Cycle-Accurate Worst-Case Execution Time Analysis. In Proceedings of the 2006 IEEE Design and Diagnostics of Electronic Circuits and systems (DDECS ’06).