{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:17:48Z","timestamp":1742933868920,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175805"},{"type":"electronic","value":"9783319175812"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17581-2_16","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T12:22:36Z","timestamp":1429100556000},"page":"239-255","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Spin-Based Approach for Checking OSEK\/VDX Applications"],"prefix":"10.1007","author":[{"given":"Haitao","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Toshiaki","family":"Aoki","sequence":"additional","affiliation":[]},{"given":"Yuki","family":"Chiba","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"unstructured":"Trampoline. http:\/\/trampoline.rts-software.org\/","key":"16_CR1"},{"issue":"11","key":"16_CR2","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"152","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A.: Model checking: algorithmic verification and debugging. Commun. ACM 152(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"issue":"5","key":"16_CR3","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans Program. Lang. Syst."},{"key":"16_CR4","volume-title":"Real-Time Systems and Programming Languages","author":"A Burns","year":"2009","unstructured":"Burns, A., Wellings, A.: Real-Time Systems and Programming Languages, 4th edn. Addison Wesley Longmain, New York (2009)","edition":"4"},{"issue":"11","key":"16_CR5","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Clarke, E.M., Zhu, Y.: Bounded model checking. Adv. Comput. 58(11), 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Lucent Technologies Inc., Bell Laboratories, Boston, USA (2003)","key":"16_CR6"},{"doi-asserted-by":"crossref","unstructured":"Zhang, H., Aoki, T., et al.: An approach for checking OSEK\/VDX applications. In: 13th QSIC, pp. 113\u2013116 (2013)","key":"16_CR7","DOI":"10.1109\/QSIC.2013.62"},{"doi-asserted-by":"crossref","unstructured":"Zhang, H., Aoki, T., Lin, H.-H., et al.: SMT-based bounded model checking for OSEK\/VDX applications. In: 20th APSEC, vol. 2(4), pp. 307\u2013314 (2013)","key":"16_CR8","DOI":"10.1109\/APSEC.2013.49"},{"doi-asserted-by":"crossref","unstructured":"Chen, J., Aoki, T.: Conformance testing for OSEK\/VDX operating system using model checking. In: 18th Asia Pacific, pp. 274\u2013281 (2011)","key":"16_CR9","DOI":"10.1109\/APSEC.2011.26"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-16164-3_5","volume-title":"Model Checking Software","author":"K Yatake","year":"2010","unstructured":"Yatake, K., Aoki, T.: Automatic generation of model checking scripts based on environment modeling. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 58\u201375. Springer, Heidelberg (2010)"},{"unstructured":"Lemieux, J.: Programming in the OSEK\/VDX Environment. CMP, Suite 200 Lawrence, KS 66046, USA (2001)","key":"16_CR11"},{"issue":"1","key":"16_CR12","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanzlek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39\u201365 (2008)","journal-title":"Real-Time Syst."},{"unstructured":"OSEK\/VDX Group: OSEK\/VDX operating system specification 2.2.3. http:\/\/portal.osek-vdx.org\/","key":"16_CR13"},{"doi-asserted-by":"crossref","unstructured":"Stoller, S.D.: Model-checking multi-threaded distributed java programs. In: 7th International SPIN Workshop, pp. 224\u2013244 (2000)","key":"16_CR14","DOI":"10.1007\/10722468_14"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Huang, Y., Zhao, Y., et al.: Modeling and verifying the code-level OSEK\/VDX operating system with CSP. In: 5th Theoretical Aspects of Software Engineering (TASE), pp. 142\u2013149 (2011)","key":"16_CR16","DOI":"10.1109\/TASE.2011.11"},{"doi-asserted-by":"crossref","unstructured":"Choi, Y.: Safety analysis of trampoline os using model checking: an experience report. In: Software Reliability Engineering (ISSRE), pp. 200\u2013209 (2011)","key":"16_CR17","DOI":"10.1109\/ISSRE.2011.22"},{"issue":"1","key":"16_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1455229.1455239","volume":"14","author":"Z Yang","year":"2009","unstructured":"Yang, Z., Wang, C., Gupta, A., et al.: Model checking sequential software programs via mixed symbolic analysis. ACM Trans. Des. Autom. Electron. Syst. 14(1), 1\u201326 (2009)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17581-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T23:46:11Z","timestamp":1676936771000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17581-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175805","9783319175812"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17581-2_16","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}