[Master] Exploration by model-checking of timing anomaly cancellation in a processor

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.

Documents joints

Timing Anomalies by Model-Checking

12 octobre 2022
info document : PDF
68 kio

Contact | Plan du site | Site réalisé avec SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 3982924