Advisers: Lionel Rieg, Catherine Vigouroux
Safe timing analysis in critical systems relies on the composition of local worst cases: the global worst case is built from local worst cases for each component. Unfortunately, this methodology is not sound in general, as the local worst cases do not always lead to the global one, which is called a timing anomaly.
The goal of this internship is to study the long-term effect of timing anomalies using a processor model developped in a model-checker (a tool to formally verify properties on a model). In particular, experiments suggest that the effect of timing anomalies eventually gets cancelled. We want to investigate this aspect more.
More detail is available in the attached pdf description.
