Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture

Static worst-case timing analyses compute safe timing bounds of applications running in real-time systems. These bounds are necessary to evaluate the strict timing constraints of real-time systems. Moreover, the inherent complexity of such systems demands that their timing analyses are able to cope with the large resulting state space. In this direction, a potential solution is to perform compositional timing analysis, where the system-level timing is obtained from component-level timings. Undesired timing phenomena, called timing anomalies, threaten the soundness of (compositional) timing analyses. In this work, we investigate how the industrial superscalar TriCore architecture is amenable for compositional timing analyses via a formal evaluation of amplification timing anomalies. Firstly, we adapt and extend a specialized abstraction, called canonical pipeline model, to capture the amplification effects in a formal model of the TriCore architecture. Then, we use model checking to efficiently detect amplification timing anomalies and report the associated complexity results. Finally, we aim for better precision as we design and implement counterexample-based methods so as to uncover patterns leading to such anomalies.