{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T14:12:24Z","timestamp":1766067144156},"reference-count":17,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2020,4,1]]},"DOI":"10.1587\/transinf.2019edp7172","type":"journal-article","created":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T22:25:19Z","timestamp":1585693519000},"page":"800-812","source":"Crossref","is-referenced-by-count":7,"title":["Model Checking of Real-Time Properties for Embedded Assembly Program Using Real-Time Temporal Logic RTCTL and Its Application to Real Microcontroller Software"],"prefix":"10.1587","volume":"E103.D","author":[{"given":"Yajun","family":"WU","sequence":"first","affiliation":[{"name":"Graduate School of Natural Science and Technology, Kanazawa University"}]},{"given":"Satoshi","family":"YAMANE","sequence":"additional","affiliation":[{"name":"Graduate School of Natural Science and Technology, Kanazawa University"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] R. Jhala and R. Majumdar, \u201cSoftware model checking,\u201d ACM Computing Surveys (CSUR), vol.41, no.4, 2009. 10.1145\/1592434.1592438","DOI":"10.1145\/1592434.1592438"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] L. de Moura and N. Bj\u00f8rner, \u201cZ3: An Efficient SMT Solver,\u201d LNCS, vol.4963, pp.337-340, 2008. 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] S. Yamane, R. Konoshita, and T. Kato, \u201cModel checking of embedded assembly program based on simulation,\u201d IEICE Trans. Inf. & Syst., vol.E100-D, no.8, pp.1819-1826, 2017. 10.1587\/transinf.2016edp7452","DOI":"10.1587\/transinf.2016EDP7452"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] B. Schlich, \u201cModel Checking of Software for Microcontrollers,\u201d ACM Transactions on Embedded Computing Systems, vol.9, no.4, 2010. 10.1145\/1721695.1721702","DOI":"10.1145\/1721695.1721702"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] J. Kobashi, S. Yamane, and A. Takeshita, \u201cDevelopment of SMT-Based Bounded Model Checker for embedded assembly program,\u201d GCCE 2014, pp.696-698, 2014. 10.1109\/gcce.2014.7031120","DOI":"10.1109\/GCCE.2014.7031120"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] M. Kuo, R. Sinha, and P. Roop, \u201cEfficient WCRT analysis of synchronous programs using reachability,\u201d 48th ACM\/EDAC\/IEEE Design Automation Conference (DAC), pp.480-485, 2011. 10.1145\/2024724.2024837","DOI":"10.1145\/2024724.2024837"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan, \u201cQuantitative Temporal Reasoning,\u201d Real-Time Systems, vol.4, no.4, pp.331-352, 1992. 10.1007\/bf00355298","DOI":"10.1007\/BF00355298"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[8] R. Alur and D.L. Dill, \u201cA theory of timed automata,\u201d TCS, vol.126, no.2, pp.183-235, 1994. 10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"9","unstructured":"[9] P. Bouyer, U. Fahrenberg, K.G. Larsen, N. Markey, J. Ouaknine, and J. Worrell, \u201cModel checking real-time systems. In Handbook of Model Checking,\u201d pp.1001-1046, Springer, Cham, 2018."},{"key":"10","doi-asserted-by":"crossref","unstructured":"[10] M.H. Moghadam, M. Saadatmand, M. Borg, M. Bohlin, and B. Lisper, \u201cLearning-based Response Time Analysis in Real-Time Embedded Systems: A Simulation-based Approach,\u201d ACM\/IEEE 1st International Workshop on Software Qualities and their Dependencies, pp.21-24, 2018. 10.1145\/3194095.3194097","DOI":"10.1145\/3194095.3194097"},{"key":"11","unstructured":"[11] J.-L. B\u00e9chennec and F. Cassez, \u201cComputation of wcet using program slicing and real-time model-checking.\u201d arXiv preprint arXiv:1105.1633, 2011."},{"key":"12","unstructured":"[12] S.A. Kripke, \u201cSemantical Considerations on Modal Logic,\u201d Acta Philosophica Fennica, 16, pp.83-94, 1963."},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] E.M. Clarke and E.A. Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, LNCS 131, pp.52-71, 1981.","DOI":"10.1007\/BFb0025774"},{"key":"14","unstructured":"[14] R.E. Corporation, Renesas Electronics, Renesas Electronics Corporation (online), http:\/\/japan.renesas.com\/"},{"key":"15","unstructured":"[15] nuvo WHEEL: ZMP, http:\/\/www.zmp.co.jp\/products\/wheel"},{"key":"16","unstructured":"[16] G. Klein, JFlex-The Fast Scanner Generator for Java, CSE UNSW (online), available from ( http:\/\/jflex.de\/ )"},{"key":"17","unstructured":"[17] M.P. Jones, Jacc: just another compiler compiler for Java, Department of Computer Science and Engineering at the OGI School of Science & Engineering at OHSU (online), available from ( http:\/\/jflex.de\/ )"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E103.D\/4\/E103.D_2019EDP7172\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T03:28:17Z","timestamp":1585970897000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E103.D\/4\/E103.D_2019EDP7172\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,1]]},"references-count":17,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2019edp7172","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,1]]}}}