[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.

Attached documents

Timing Anomalies by Model-Checking

12 October 2022
info document : PDF
68 KiB

Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 3988511