{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,21]],"date-time":"2024-03-21T16:01:54Z","timestamp":1711036914383},"reference-count":29,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"10","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2015]]},"DOI":"10.1587\/transinf.2015edp7043","type":"journal-article","created":{"date-parts":[[2015,9,30]],"date-time":"2015-09-30T18:07:41Z","timestamp":1443636461000},"page":"1765-1776","source":"Crossref","is-referenced-by-count":3,"title":["Verifying OSEK\/VDX Applications: A Sequentialization-Based Model Checking Approach"],"prefix":"10.1587","volume":"E98.D","author":[{"given":"Haitao","family":"ZHANG","sequence":"first","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toshiaki","family":"AOKI","sequence":"additional","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuki","family":"CHIBA","sequence":"additional","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"[1] H. Zhang, T. Aoki, and Y. Chiba, \u201cYes! You Can Use Your Model Checker to Verify OSEK\/VDX Applications,\u201d accepted by IEEE International Conference on Software Testing, Verification and Validation (ICST), Graz, April 2015.","DOI":"10.1109\/ICST.2015.7102612"},{"key":"2","unstructured":"[2] J. Lemieux, Programming in the OSEK\/VDX Environment, CMP, Suite 200 Lawrence, KS 66046, USA, 2001."},{"key":"3","unstructured":"[3] OSEK\/VDX Group, \u201cOSEK\/VDX operating system specification 2.2.3,\u201d http:\/\/portal.osek-vdx.org\/, accessed May. 10. 2015."},{"key":"4","unstructured":"[4] E.M. Clarke, O. Grumberg, and D.E. Long, \u201cModel Checking and Abstraction,\u201d ACM Trans. Programming Languages and Systems (TOPLAS), vol.16, no.5, pp.1512-1542, Sept. 1994."},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] E.M. Clarke, E.A. Emerson, and J. Sifakis, \u201cModel Checking: Algorithmic Verification and Debugging,\u201d Commun. ACM, vol.52, no.11, pp.74-84, Nov. 2009.","DOI":"10.1145\/1592761.1592781"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] Z. Yang, C. Wang, A. Gupta, and I. Franjo, \u201cModel Checking Sequential Software Programs Via Mixed Symbolic Analysis,\u201d ACM Trans. Design Automation of Electronic Systems, vol.14, no.1, pp.1-26, Jan. 2009.","DOI":"10.1145\/1455229.1455239"},{"key":"7","unstructured":"[7] A. Cimatti, A. Micheli, I. Narasamdya, and M. Roveri, \u201cVerifying SystemC: A software model checking approach,\u201d FMCAD, pp.51-59, Oct. 2010."},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] L. Cordeiro and B. Fischer, \u201cVerifying Multi-threaded Software using SMT-based Context-Bounded Model Checking,\u201d ICSE, vol.3, no.9, pp.331-340, May 2011.","DOI":"10.1145\/1985793.1985839"},{"key":"9","unstructured":"[9] SystemC standard, \u201cIEEE 1666: SystemC language Reference Manual,\u201d 2005."},{"key":"10","unstructured":"[10] H. Zhang, T. Aoki, and Y. Chiba, \u201cA Spin-based Approach for Checking OSEK\/VDX Applications,\u201d 3rd International Workshop FTSCS in ICFEM, pp.187-202, Nov. 2014."},{"key":"11","unstructured":"[11] G.J. Holzmann, The Spin Model Checker: Primer and Reference Manual, Lucent Technologies Inc., Bell Laboratories, Boston, USA, Sept. 2003."},{"key":"12","unstructured":"[12] E.M. Clarke, W. Klieber, et al., \u201cModel Checking and the State Explosion Problem,\u201d Tools for Practical Software Verification, vol.7682, pp.1-30, 2012."},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] H. Zhang, T. Aoki, H.-H. Lin, M. Zhang, Y. Chiba, and K. Yatake, \u201cSMT-based Bounded Model Checking for OSEK\/VDX Applications,\u201d 20th APSEC, pp.307-314, Dec. 2013.","DOI":"10.1109\/APSEC.2013.49"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] H. Zhang, T. Aoki, K. Yatake, M. Zhang, and H.-H. Lin, \u201cAn Approach for Checking OSEK\/VDX Applications,\u201d 13th QSIC, pp.113-116, July 2013.","DOI":"10.1109\/QSIC.2013.62"},{"key":"15","doi-asserted-by":"crossref","unstructured":"[15] A. Armando, J. Mantovani, and L. Platania, \u201cBounded model checking of software using SMT solvers instead of SAT solvers,\u201d STTT, vol.11, no.1, pp.69-83, 2009.","DOI":"10.1007\/s10009-008-0091-0"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] A. Biere, A. Cimatti, E.M. Clarke, O. Strichman, and Y. Zhu, \u201cBounded Model Checking,\u201d Advances in Computers, vol.58, no.11, pp.117-148, 2003.","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"17","unstructured":"[17] Uppsala University, Sweden and Aalborg University, \u201cUPPAAL,\u201d http:\/\/www.uppaal.org\/"},{"key":"18","unstructured":"[18] A. Burns and A. Wellings, Real-Time Systems and Programming Languages (4th Edition), Addison Wesley Longmain, New York, NY, USA, Aug. 2009."},{"key":"19","unstructured":"[19] G. Necula, \u201cCIL,\u201d http:\/\/kerneis.github.io\/cil\/, accessed May. 10. 2015."},{"key":"20","unstructured":"[20] T.H. Khan, A. Habibi, et al., \u201cA Tool for Converting Finite State Machines to SystemC,\u201d Technical Report, Concordia University, Canada, 2007."},{"key":"21","unstructured":"[21] P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, PhD thesis, University of Liege, Computer Science Department, Nov. 1994."},{"key":"22","doi-asserted-by":"crossref","unstructured":"[22] J. Chen and T. Aoki, \u201cConformance Testing for OSEK\/VDX Operating System Using Model Checking,\u201d 18th APSEC, pp.274-281, 2011.","DOI":"10.1109\/APSEC.2011.26"},{"key":"23","doi-asserted-by":"crossref","unstructured":"[23] K. Yatake and T. Aoki, \u201cAutomatic Generation of Model Checking Scripts Based on Environment Modeling,\u201d SPIN, pp.58-75, 2010.","DOI":"10.1007\/978-3-642-16164-3_5"},{"key":"24","unstructured":"[24] IRCCyN group, \u201cTrampoline,\u201d http:\/\/trampoline.rts-software.org\/, accessed May. 10. 2015."},{"key":"25","doi-asserted-by":"crossref","unstructured":"[25] Y. Choi, \u201cSafety Analysis of Trampoline OS Using Model Checking: An Experience Report,\u201d Software Reliability Engineering (ISSRE), pp.200-209, Nov. 2011.","DOI":"10.1109\/ISSRE.2011.22"},{"key":"26","doi-asserted-by":"crossref","unstructured":"[26] Y. Huang, Y. Zhao, L. Zhu, Q. Li, H. Zhu, and J. Shi, \u201cModeling and Verifying the Code-Level OSEK\/VDX Operating System with CSP,\u201d 5th IEEE Trans. Autom. Sci. Eng., pp.142-149, 2011.","DOI":"10.1109\/TASE.2011.11"},{"key":"27","doi-asserted-by":"crossref","unstructured":"[27] L. Waszniowski and Z. Hanz\u00e1lek, \u201cFormal verification of multitasking applications based on timed automata model,\u201d Real-Time Systems, pp.39-65, 2008.","DOI":"10.1007\/s11241-007-9036-z"},{"key":"28","doi-asserted-by":"crossref","unstructured":"[28] O. Inverso, E. Tomasco, B. Fischer, S.L. Torre, and G. Parlato, \u201cLazy-CSeq: A Lazy Sequentialization Tool for C,\u201d 20th TACAS, pp.398-401, 2014.","DOI":"10.1007\/978-3-642-54862-8_29"},{"key":"29","unstructured":"[29] ISO\/IEC, \u201cInformation technology-Portable Operating System Interface (POSIX) Base Specifications,\u201d Issue 7, ISO\/IEC\/IEEE 9945: 2009, ISO, 2009."}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E98.D\/10\/E98.D_2015EDP7043\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,31]],"date-time":"2019-08-31T00:24:04Z","timestamp":1567211044000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E98.D\/10\/E98.D_2015EDP7043\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":29,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2015]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2015edp7043","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}