{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,13]],"date-time":"2024-03-13T21:12:04Z","timestamp":1710364324159},"reference-count":33,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"8","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2020,8,1]]},"DOI":"10.1587\/transinf.2019fop0002","type":"journal-article","created":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T22:17:47Z","timestamp":1596233867000},"page":"1794-1805","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking of Automotive Control Software: An Industrial Approach"],"prefix":"10.1587","volume":"E103.D","author":[{"given":"Masahiro","family":"MATSUBARA","sequence":"first","affiliation":[{"name":"Hitachi Automotive Systems, Ltd."},{"name":"Graduate School of Information Science and Technology, Osaka University"}]},{"given":"Tatsuhiro","family":"TSUCHIYA","sequence":"additional","affiliation":[{"name":"Graduate School of Information Science and Technology, Osaka University"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"[1] D. Engler and M. Musuvathi, \u201cStatic Analysis versus Software Model Checking for Bug Finding,\u201d Verification, Model Checking, and Abstract Interpretation, ed. B. Steffen and G. Levi, Berlin, Heidelberg, vol.2937, pp.191-210, Springer Berlin Heidelberg, 2004. 10.1007\/978-3-540-24622-0_17","DOI":"10.1007\/978-3-540-24622-0_17"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] A. Min\u00e9, \u201cStatic Analysis of Embedded Real-Time Concurrent Software with Dynamic Priorities,\u201d Electronic Notes in Theoretical Computer Science, vol.331, pp.3-39, March 2017. 10.1016\/j.entcs.2017.02.002","DOI":"10.1016\/j.entcs.2017.02.002"},{"key":"3","unstructured":"[3] E.M. Clarke, O. Grumberg, D. Kroening, D.A. Peled, and H. Veith, Model checking, MIT Press, 2018."},{"key":"4","unstructured":"[4] M. Mansouri-Samani, P.C. Mehlitz, C.S. Pasareanu, J.J. Penix, G.P. Brat, L.Z. Markosian, O. O'Malley, T.T. Pressburger, and W.C. Visser, \u201cProgram Model Checking: A Practitioner's Guide,\u201d 2008."},{"key":"5","unstructured":"[5] G.J. Holzmann, The SPIN Model Checker-primer and reference manual, Addison-Wesley, 2004."},{"key":"6","doi-asserted-by":"publisher","unstructured":"[6] Z. Chen, Y. Gu, Z. Huang, J. Zheng, C. Liu, and Z. Liu, \u201cModel checking aircraft controller software: A case study,\u201d Software-Practice and Experience, vol.45, no.7, pp.989-1017, 2015. 10.1002\/spe.2242","DOI":"10.1002\/spe.2242"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] T. Ovatman, A. Aral, D. Polat, and A.O. \u00dcnver, \u201cAn overview of model checking practices on verification of PLC software,\u201d Software and Systems Modeling, vol.15, no.4, pp.937-960, 2016. 10.1007\/s10270-014-0448-7","DOI":"10.1007\/s10270-014-0448-7"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[8] S.T. Hamman, K.M. Hopkinson, and J.E. Fadul, \u201cA Model Checking Approach to Testing the Reliability of Smart Grid Protection Systems,\u201d IEEE Transactions on Power Delivery, vol.32, no.6, pp.2408-2415, 2017. 10.1109\/tpwrd.2016.2635480","DOI":"10.1109\/TPWRD.2016.2635480"},{"key":"9","unstructured":"[9] M. Weiser, \u201cProgram Slicing,\u201d Proceedings of the International Conference on Software Engineering (ICSE '81), pp.439-449, 1981."},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] B. Xu, J. Qian, X. Zhang, Z. Wu, and L. Chen, \u201cA brief survey of program slicing,\u201d ACM SIGSOFT Software Engineering Notes, vol.30, no.2, pp.1-36, 2005. 10.1145\/1050849.1050865","DOI":"10.1145\/1050849.1050865"},{"key":"11","doi-asserted-by":"publisher","unstructured":"[11] J. Silva, \u201cA Vocabulary of Program Slicing-based Techniques,\u201d ACM Comput. Surv., vol.44, no.3, pp.12:1-12:41, 2012. 10.1145\/2187671.2187674","DOI":"10.1145\/2187671.2187674"},{"key":"12","doi-asserted-by":"publisher","unstructured":"[12] D. Binkley, N. Gold, and M. Harman, \u201cAn empirical study of static program slice size,\u201d ACM Transactions on Software Engineering and Methodology, vol.16, no.2, pp.1-32, 2007. 10.1145\/1217295.1217297","DOI":"10.1145\/1217295.1217297"},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] J. Krinke, \u201cStatic slicing of threaded programs,\u201d 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp.35-42, 1998. 10.1145\/277631.277638","DOI":"10.1145\/277633.277638"},{"key":"14","unstructured":"[14] D. Hisley, M.J. Bridges, and L.L. Pollock, \u201cStatic Interprocedural Slicing of Shared Memory Parallel Programs,\u201d Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications-Volume 2, PDPTA '02, pp.658-664, CSREA Press, 2002."},{"key":"15","doi-asserted-by":"crossref","unstructured":"[15] J. Krinke, \u201cContext-sensitive slicing of concurrent programs,\u201d Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering (ESEC\/FSE-11), pp.178-187, 2003. 10.1145\/940071.940096","DOI":"10.1145\/940071.940096"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] J. Ferrante, K.J. Ottenstein, and J.D. Warren, \u201cThe program dependence graph and its use in optimization,\u201d International Symposium on Programming, LNCS, vol.167, pp.125-132, 1984. 10.1007\/3-540-12925-1_33","DOI":"10.1007\/3-540-12925-1_33"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] J. Ferrante, K.J. Ottenstein, and J.D. Warren, \u201cThe Program Dependence Graph and Its Use in Optimization,\u201d ACM Trans. Program. Lang. Syst., vol.9, no.3, pp.319-349, 1987. 10.1145\/24039.24041","DOI":"10.1145\/24039.24041"},{"key":"18","doi-asserted-by":"crossref","unstructured":"[18] S. Horwitz and T. Reps, \u201cThe use of program dependence graphs in software engineering,\u201d Proceedings of the 14th International Conference on Software Engineering, ICSE'92, New York, NY, USA, pp.392-411, Association for Computing Machinery, 1992. 10.1145\/143062.143156","DOI":"10.1145\/143062.143156"},{"key":"19","doi-asserted-by":"crossref","unstructured":"[19] M. Florian, E. Gamble, and G. Holzmann, \u201cLogic Model Checking of Time-Periodic Real-Time Systems,\u201d Infotech@Aerospace 2012, 2012. 10.2514\/6.2012-2607","DOI":"10.2514\/6.2012-2607"},{"key":"20","doi-asserted-by":"crossref","unstructured":"[20] M.B. Dwyer, J. Hatcliff, M. Hoosier, V. Ranganath, Robby, and T. Wallentine, \u201cEvaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs,\u201d Tools and Algorithms for the Construction and Analysis of Systems, ed. H. Hermanns and J. Palsberg, Berlin, Heidelberg, vol.3920, pp.73-89, Springer Berlin Heidelberg, 2006. 10.1007\/11691372_5","DOI":"10.1007\/11691372_5"},{"key":"21","doi-asserted-by":"crossref","unstructured":"[21] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. P\u0103s\u0103reanu, Robby, and H. Zheng, \u201cBandera: Extracting Finite-state Models from Java Source Code,\u201d Proceedings of the 22Nd International Conference on Software Engineering, ICSE '00, New York, NY, USA, pp.439-448, ACM, 2000. 10.1145\/337180.337234","DOI":"10.1145\/337180.337234"},{"key":"22","doi-asserted-by":"publisher","unstructured":"[22] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, \u201cModel Checking Programs,\u201d Automated Software Engineering, vol.10, no.2, pp.203-232, 2003. 10.1023\/a:1022920129859","DOI":"10.1023\/A:1022920129859"},{"key":"23","doi-asserted-by":"crossref","unstructured":"[23] G.J. Holzmann and T.C. Ruys, \u201cEffective Bug Hunting with Spin and Modex,\u201d Model Checking Software, ed. P. Godefroid, Berlin, Heidelberg, p.24, Springer Berlin Heidelberg, 2005. 10.1007\/11537328_3","DOI":"10.1007\/11537328_3"},{"key":"24","doi-asserted-by":"crossref","unstructured":"[24] M. Ichii, T. Myojin, Y. Nakagawa, M. Chikahisa, and H. Ogawa, \u201cA Rule-based Automated Approach for Extracting Models from Source Code,\u201d 2012 19th Working Conference on Reverse Engineering, pp.308-317, 2012. 10.1109\/wcre.2012.40","DOI":"10.1109\/WCRE.2012.40"},{"key":"25","doi-asserted-by":"crossref","unstructured":"[25] D. Giffhorn and C. Hammer, \u201cAn Evaluation of Slicing Algorithms for Concurrent Programs,\u201d Seventh IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2007), pp.17-26, 2007. 10.1109\/scam.2007.9","DOI":"10.1109\/SCAM.2007.9"},{"key":"26","doi-asserted-by":"publisher","unstructured":"[26] D. Giffhorn and C. Hammer, \u201cPrecise slicing of concurrent programs,\u201d Automated Software Engineering, vol.16, no.2, pp.197-234, 2009. 10.1007\/s10515-009-0048-x","DOI":"10.1007\/s10515-009-0048-x"},{"key":"27","doi-asserted-by":"publisher","unstructured":"[27] M.G. Nanda and S. Ramesh, \u201cInterprocedural Slicing of Multithreaded Programs with Applications to Java,\u201d ACM Trans. Program. Lang. Syst., vol.28, no.6, pp.1088-1144, 2006. 10.1145\/1186632.1186636","DOI":"10.1145\/1186632.1186636"},{"key":"28","unstructured":"[28] J. Krinke, \u201cVisualization of program dependence and slices,\u201d IEEE International Conference on Software Maintenance, ICSM, pp.168-177, 2004. 10.1109\/icsm.2004.1357801"},{"key":"29","doi-asserted-by":"publisher","unstructured":"[29] J. Krinke, \u201cSlicing, chopping, and path conditions with barriers,\u201d Software Quality Journal, vol.12, no.4, pp.339-360, 2004. 10.1023\/b:sqjo.0000039792.93414.a5","DOI":"10.1023\/B:SQJO.0000039792.93414.a5"},{"key":"30","unstructured":"[30] K. Chen and V. Rajlich, \u201cCase study of feature location using dependence graph,\u201d Proceedings IWPC 2000. 8th International Workshop on Program Comprehension, pp.241-247, 2000. 10.1109\/wpc.2000.852498"},{"key":"31","doi-asserted-by":"publisher","unstructured":"[31] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith,\u201cCounterexample-Guided Abstraction Refinement for Symbolic Model Checking,\u201d Journal of the ACM, vol.50, no.5, pp.752-794, 2003. 10.1145\/876638.876643","DOI":"10.1145\/876638.876643"},{"key":"32","doi-asserted-by":"publisher","unstructured":"[32] D. Beyer, T.A. Henzinger, R. Jhala, and R. Majumdar, \u201cThe software model checker Blast,\u201d International Journal on Software Tools for Technology Transfer, vol.9, no.5-6, pp.505-525, 2007. 10.1007\/s10009-007-0044-z","DOI":"10.1007\/s10009-007-0044-z"},{"key":"33","doi-asserted-by":"publisher","unstructured":"[33] T. Ball, V. Levin, and S.K. Rajamani, \u201cA decade of software model checking with SLAM,\u201d Communications of the ACM, vol.54, no.7, pp.68-76, 2011. 10.1145\/1965724.1965743","DOI":"10.1145\/1965724.1965743"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E103.D\/8\/E103.D_2019FOP0002\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,1]],"date-time":"2020-08-01T03:24:35Z","timestamp":1596252275000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E103.D\/8\/E103.D_2019FOP0002\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,1]]},"references-count":33,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2020]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2019fop0002","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,1]]}}}