{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:44:51Z","timestamp":1747248291588},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T00:00:00Z","timestamp":1649635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T00:00:00Z","timestamp":1649635200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,6]]},"DOI":"10.1007\/s10009-022-00655-1","type":"journal-article","created":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T06:03:42Z","timestamp":1649657022000},"page":"415-440","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture"],"prefix":"10.1007","volume":"24","author":[{"given":"Benjamin","family":"Binder","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mihail","family":"Asavoae","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Brandner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Belgacem","family":"Ben Hedia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathieu","family":"Jan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,4,11]]},"reference":[{"key":"655_CR1","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-96145-3_15","volume-title":"Computer Aided Verification","author":"A Abate","year":"2018","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 270\u2013288. Springer International Publishing, Cham (2018)"},{"key":"655_CR2","unstructured":"Asavoae, M., Ben Hedia, B., Jan, M.: Formal executable models for automatic detection of timing anomalies. In: 18th International Workshop on Worst-Case Execution Time Analysis (WCET), Barcelona, Spain, pp. 2:1\u20132:13, (2018)"},{"key":"655_CR3","doi-asserted-by":"crossref","unstructured":"Ballabriga, C., Cass\u00e9, H., Rochange, C., Sainrat, P.: OTAWA: an open toolbox for adaptive WCET analysis. In: SEUS 2010. pp. 35\u201346 (2010)","DOI":"10.1007\/978-3-642-16256-5_6"},{"key":"655_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories, pp. 305\u2013343. Springer International Publishing, Cham (2018). 10.1007\/978-3-319-10575-8_11,","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"655_CR5","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-58298-2_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"B Binder","year":"2020","unstructured":"Binder, B., Asavoae, M., Brandner, F., Ben Hedia, B., Jan, M.: Scalable detection of amplification timing anomalies for the superscalar tricore architecture. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) Formal Methods for Industrial Critical Systems, pp. 151\u2013169. Springer International Publishing, Cham (2020)"},{"key":"655_CR6","unstructured":"Bj\u00f8rner, N., de\u00a0Moura, L., Nachmanson, L., Wintersteiger, C.: Programming z3. http:\/\/theory.stanford.edu\/~nikolaj\/programmingz3.html"},{"key":"655_CR7","doi-asserted-by":"crossref","unstructured":"Brady, B.A., Holcomb, D., Seshia, S.A.: Counterexample-guided smt-driven optimal buffer sizing. In: 2011 Design, Automation Test in Europe. pp.\u00a01\u20136 (2011). 10.1109\/DATE.2011.5763058","DOI":"10.1109\/DATE.2011.5763058"},{"key":"655_CR8","doi-asserted-by":"crossref","unstructured":"de\u00a0Dinechin, B.D., van Amstel, D., Poulhi\u00e8s, M., Lager, G.: Time-critical computing on a single-chip massively parallel processor. In: Proceedings of the Conference on Design, Automation & Test in Europe (DATE\u201914). pp. 97:1\u201397:6 (2014)","DOI":"10.7873\/DATE2014.110"},{"key":"655_CR9","unstructured":"Eisinger, J., Polian, I., Becker, B., Metzner, A., Thesing, S., Wilhelm, R.: Automatic identification of timing anomalies for cycle-accurate worst-case execution time analysis. In: Proceedings of the Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS). Prague, Czech Republic, pp. 15\u201320. (2006)"},{"key":"655_CR10","doi-asserted-by":"crossref","unstructured":"Hahn, S., Reineke, J.: Design and analysis of sic: A provably timing-predictable pipelined processor core. In: 2018 IEEE Real-Time Systems Symposium (RTSS). pp. 469\u2013481 (2018)","DOI":"10.1109\/RTSS.2018.00060"},{"key":"655_CR11","doi-asserted-by":"crossref","unstructured":"Hahn, S., Jacobs, M., Reineke, J.: Enabling compositionality for multicore timing analysis. In: Plantec, A., Singhoff, F., Faucou, S., Pinho, L.M. (eds.) Proceedings of the 24th International Conference on Real-Time Networks and Systems, RTNS 2016, Brest, France, October 19-21, 2016. pp. 299\u2013308. ACM (2016)","DOI":"10.1145\/2997465.2997471"},{"issue":"1","key":"655_CR12","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/2752801.2752805","volume":"12","author":"S Hahn","year":"2015","unstructured":"Hahn, S., Reineke, J., Wilhelm, R.: Towards compositionality in execution time analysis: Definition and challenges. SIGBED Rev. 12(1), 28\u201336 (2015)","journal-title":"SIGBED Rev."},{"key":"655_CR13","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer architecture - A quantitative approach, 5th Edition. Morgan Kaufmann (2012)"},{"key":"655_CR14","unstructured":"Infineon Technologies AG: Architecture Overview Handbook, TriCore 1.3, 32-bit Unified Processor Core, IP Cores (05 2002)"},{"key":"655_CR15","unstructured":"Infineon technologies AG: TriCore 1 pipeline behaviour and instruction execution timing (2004)"},{"key":"655_CR16","unstructured":"Infineon Technologies AG: AURIX TC21x\/TC22x\/TC23x Family 32-Bit Single-Chip Microcontroller User\u2019s Manual (12 2014)"},{"key":"655_CR17","doi-asserted-by":"crossref","unstructured":"Jan, M., Asavoae, M., Schoeberl, M., Lee, E.: Formal semantics of predictable pipelines: a comparative study. In: Proceedings of the 25th Asia and South Pacific Design Automation Conference. IEEE, United States (2020)","DOI":"10.1109\/ASP-DAC47756.2020.9045351"},{"key":"655_CR18","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings. pp. 142\u2013159 (2002)","DOI":"10.1007\/3-540-36126-X_9"},{"key":"655_CR19","unstructured":"Lauterbach GmbH: Simulator for TriCore (04 2021)"},{"key":"655_CR20","doi-asserted-by":"crossref","unstructured":"Liu, I., Reineke, J., Lee, E.A.: A PRET architecture supporting concurrent programs with composable timing properties. In: 44th Asilomar Conference on Signals, Systems, and Computers (November 2010)","DOI":"10.1109\/ACSSC.2010.5757922"},{"key":"655_CR21","unstructured":"Lundqvist, T., Stenstr\u00f6m, P.: Timing anomalies in dynamically scheduled microprocessors. In: Real-Time Systems Symposium. pp. 12\u201321. RTSS\u201999, IEEE (1999). 10.1109\/REAL.1999.818824"},{"key":"655_CR22","unstructured":"Nguyen, V.a., Jenn, E., Serwe, W., Lang, F., Mateescu, R.: Using model checking to identify timing interferences on multicore processors. In: ERTS 2020 - 10th European Congress on Embedded Real Time Software and Systems. pp. 1\u201310. Toulouse, France (2020)"},{"key":"655_CR23","unstructured":"Reineke, J., Wachter, B., Thesing, S., Wilhelm, R., Polian, I., Eisinger, J., Becker, B.: A definition and classification of timing anomalies. In: 6th International Workshop on Worst-Case Execution Time (WCET) Analysis. Dresden, Germany (2006)"},{"key":"655_CR24","doi-asserted-by":"crossref","unstructured":"Schoeberl, M., Abbaspour, S., Akesson, B., Audsley, N.C., Capasso, R., Garside, J., Goossens, K., Goossens, S., Hansen, S., Heckmann, R., Hepp, S., Huber, B., Jordan, A., Kasapaki, E., Knoop, J., Li, Y., Prokesch, D., Puffitsch, W., Puschner, P.P., Rocha, A., Silva, C., Spars\u00f8, J., Tocchi, A.: T-CREST: time-predictable multi-core architecture for embedded systems. J. Syst. Arch. Emb. Syst. Design 61(9), 449\u2013471 (2015)","DOI":"10.1016\/j.sysarc.2015.04.002"},{"key":"655_CR25","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Subramanyan, P.: Uclid5: Integrating modeling, verification, synthesis and learning. In: 2018 16th ACM\/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). pp. 1\u201310 (2018). 10.1109\/MEMCOD.2018.8556946","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"655_CR26","unstructured":"Sun, W.T., Jenn, E., Cass\u00e9, H.: Build your own static wcet analyser: the case of the automotive processor aurix tc275. In: 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020) (Jan 2020)"},{"issue":"5","key":"655_CR27","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/MM.2010.78","volume":"30","author":"T Ungerer","year":"2010","unstructured":"Ungerer, T., Cazorla, F.J., Sainrat, P., Bernat, G., Petrov, Z., Rochange, C., Qui\u00f1ones, E., Gerdes, M., Paolieri, M., Wolf, J., Cass\u00e9, H., Uhrig, S., Guliashvili, I., Houston, M., Kluge, F., Metzlaff, S., Mische, J.: Merasa: Multicore execution of hard real-time applications supporting analyzability. IEEE Micro 30(5), 66\u201375 (2010)","journal-title":"IEEE Micro"},{"key":"655_CR28","doi-asserted-by":"crossref","unstructured":"Wenzel, I., Kirner, R., Puschner, P.P., Rieder, B.: Principles of timing anomalies in superscalar processors. In: International Conference on Quality Software (QSIC 2005), Melbourne, Australia, pp. 295\u2013306. (2005)","DOI":"10.1109\/QSIC.2005.49"},{"key":"655_CR29","unstructured":"Wilhelm, S., Wachter, B.: Towards symbolic state traversal for efficient WCET analysis of abstract pipeline and cache models. In: 7th International Workshop on Worst-Case Execution Time (WCET) Analysis, Pisa, Italy, July 3, (2007)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00655-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00655-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00655-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,21]],"date-time":"2024-09-21T22:30:14Z","timestamp":1726957814000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00655-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,11]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["655"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00655-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2022,4,11]]},"assertion":[{"value":"8 March 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 April 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}