{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:23:20Z","timestamp":1750307000324,"version":"3.41.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"S2","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF 0914543"],"award-info":[{"award-number":["CCF 0914543"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:p>As multicore processors are increasingly adopted in industry, it has become a great challenge to accurately bound the worst-case execution time (WCET) for real-time systems running on multicore chips. This is particularly true because of the inter-thread interferences in accessing shared resources on multicores, such as shared L2 caches, which can significantly affect the performance but are very difficult to be estimated statically.<\/jats:p>\n          <jats:p>This article proposes an approach to analyzing WCET for multicore processors with shared L2 instruction caches by using a model checking based method. We model each concurrent real-time thread, including the inter-thread cache interferences with a PROMELA process, and derive the WCET by using a binary search algorithm. To reduce the state explosion problem, we propose several techniques for reducing the memory consumption by exploiting domain-specific information. Our experiments indicate that compared to the static analysis technique based on extended ILP (integer linear programming), our approach improves the tightness of WCET estimation by more than 31.1% for the benchmarks we studied. However, due to the inherent complexity of multicore timing analysis and the state explosion problem, the model checking based approach currently can only work with small real-time kernels for dual-core processors.<\/jats:p>","DOI":"10.1145\/2331147.2331166","type":"journal-article","created":{"date-parts":[[2012,9,11]],"date-time":"2012-09-11T22:21:06Z","timestamp":1347402066000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A Model Checking Based Approach to Bounding Worst-Case Execution Time for Multicore Processors"],"prefix":"10.1145","volume":"11","author":[{"given":"Lan","family":"Wu","sequence":"first","affiliation":[{"name":"Virginia Commonwealth University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei","family":"Zhang","sequence":"additional","affiliation":[{"name":"Virginia Commonwealth University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1289816.1289877"},{"volume":"443","volume-title":"Proceedings of the 7th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science","author":"Alur R.","key":"e_1_2_1_2_1"},{"volume-title":"Proceedings of the IEEE Real-Time Systems Symposium. 172--181","author":"Arnold R.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/268806.268810"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Clarke E. M. and Schlingloff B.-H. 2001. Model Checking Handbook of Automated Reasoning. MIT Press Cambridge MA. Clarke E. M. and Schlingloff B.-H. 2001. Model Checking Handbook of Automated Reasoning . MIT Press Cambridge MA.","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"e_1_2_1_7_1","unstructured":"CPLEX. 2010. Homepage of cplex. http:\/\/www.ilog.com\/products\/cplex. CPLEX . 2010. Homepage of cplex. http:\/\/www.ilog.com\/products\/cplex."},{"volume-title":"Proceedings of the IEEE Real-Time Systems Symposium. 288--297","author":"Healy C.","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"volume-title":"Proceedings of the 9th International Workshop on Worst-Case Execution Time (WCET) Analysis.","author":"Huber B.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217570"},{"volume-title":"Proceedings of the 17th IEEE Real-Time Systems Symposium. 254--264","author":"Li Y. S.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2004.10017"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/EUC.2008.178"},{"volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification","series-title":"Lecture Notes in Computer Science","author":"Metzner A.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391469.1391544"},{"volume-title":"Proceedings of the ACM SIGPLAN Workshop on Languages.","author":"Ottosson G.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1555754.1555764"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2007.13"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450135.1450172"},{"key":"e_1_2_1_22_1","unstructured":"SPIN 2010. Homepage of spin. http:\/\/spinroot.com\/spin\/whatispin.html. SPIN 2010. Homepage of spin. http:\/\/spinroot.com\/spin\/whatispin.html."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/502217.502240"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2005.10"},{"key":"e_1_2_1_25_1","unstructured":"Trimaran. 2010. Homepage of trimaran. http:\/\/www.trimaran.org\/. Trimaran . 2010. Homepage of trimaran. http:\/\/www.trimaran.org\/."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2004.831197"},{"volume-title":"Verification, Model Checking and Abstract Interpretation (YMCAI)","series-title":"Lecture Notes in Computer Science","author":"Wilhelm R.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2008.6"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2009.55"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2331147.2331166","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2331147.2331166","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:48:50Z","timestamp":1750236530000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2331147.2331166"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":30,"journal-issue":{"issue":"S2","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["10.1145\/2331147.2331166"],"URL":"https:\/\/doi.org\/10.1145\/2331147.2331166","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2012,8]]},"assertion":[{"value":"2009-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}