TY - GEN
T1 - Scalable Detection of Amplification Timing Anomalies for the Superscalar TriCore Architecture
AU - Binder, Benjamin
AU - Asavoae, Mihail
AU - Brandner, Florian
AU - Ben Hedia, Belgacem
AU - Jan, Mathieu
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020/1/1
Y1 - 2020/1/1
N2 - Real-time systems are subject to strong timing requirements, and thus rely on worst-case timing analyses to safely address them. Undesired timing phenomena, called timing anomalies, threaten the soundness of timing analyses. In this regard, we consider the following inauspicious partnership - a compositional timing analysis and amplification timing anomalies. Precisely, we investigate how the industrial, superscalar TriCore architecture is amenable for compositional timing analyses via a formal evaluation of amplification timing anomalies. We adapt and extend a specialized abstraction, called canonical pipeline model, to quantify the amplification effects in a model of a dual-pipelined TriCore, its asynchronous store buffer, data dependencies, and structural hazards. We use model checking to efficiently detect amplification timing anomalies and report the associated complexity results.
AB - Real-time systems are subject to strong timing requirements, and thus rely on worst-case timing analyses to safely address them. Undesired timing phenomena, called timing anomalies, threaten the soundness of timing analyses. In this regard, we consider the following inauspicious partnership - a compositional timing analysis and amplification timing anomalies. Precisely, we investigate how the industrial, superscalar TriCore architecture is amenable for compositional timing analyses via a formal evaluation of amplification timing anomalies. We adapt and extend a specialized abstraction, called canonical pipeline model, to quantify the amplification effects in a model of a dual-pipelined TriCore, its asynchronous store buffer, data dependencies, and structural hazards. We use model checking to efficiently detect amplification timing anomalies and report the associated complexity results.
KW - Model checking
KW - Timing anomalies
KW - TriCore architecture
U2 - 10.1007/978-3-030-58298-2_6
DO - 10.1007/978-3-030-58298-2_6
M3 - Conference contribution
AN - SCOPUS:85091286352
SN - 9783030582975
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 151
EP - 169
BT - Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings
A2 - ter Beek, Maurice H.
A2 - Nickovic, Dejan
PB - Springer Science and Business Media Deutschland GmbH
T2 - 25th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2020
Y2 - 2 September 2020 through 3 September 2020
ER -