{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:48:28Z","timestamp":1725749308148},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405600"},{"type":"electronic","value":"9783642405617"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40561-7_21","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T13:10:29Z","timestamp":1379509829000},"page":"305-319","source":"Crossref","is-referenced-by-count":8,"title":["Constraint Specification and Test Generation for OSEK\/VDX-Based Operating Systems"],"prefix":"10.1007","author":[{"given":"Yunja","family":"Choi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"OSEK\/VDX operating system specification 2.2.3"},{"key":"21_CR2","unstructured":"Trampoline \u2013 opensource RTOS project, http:\/\/trampoline.rts-software.org"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Chen, J., Aoki, T.: Conformance testing for OSEK\/VDX operating system using model checking. In: 18th Asia-Pacific Software Engineering Conference (2011)","DOI":"10.1109\/APSEC.2011.26"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Choi, Y.: Safety analysis of the Trampoline OS using model checking: An experience report. In: Proceedings of 22nd IEEE International Symposium on Software Reliability Engineering (2011)","DOI":"10.1109\/ISSRE.2011.22"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"de la Riva, C., Tuya, J.: Automatic generation of assumptions for modular verification of software specifications. Journal of Systems and Software (2006)","DOI":"10.1016\/j.jss.2005.11.570"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"In der Riden, T., Kanpp, S.: An approach to the pervasive formal specification and verification of an automotive system. In: Proceedings of the International Workshop on Formal Methods in Industrial Critical Systems (2005)","DOI":"10.1145\/1081180.1081195"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Lettnin, D., et al.: Semiformal verification of temporal properties in automotive hardware dependent software. In: Proceedings of Design, Automation, and Test in Europe Conference and Exhibition (April 2009)","DOI":"10.1109\/DATE.2009.5090847"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Shi, J., et al.: ORIENTAIS: Formal verified OSEK\/VDX real-time operating system. In: IEEE 17th International Conference on Engineering of Complex Computer Systems (2012)","DOI":"10.1109\/ICECCS20050.2012.6299224"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Fang, L., et al.: Formal model-based test for AUTOSAR multicore RTOS. In: Proceeding of the IEEE 5th International Conference on Software Testing, Verification and Validation, pp. 251\u2013259 (2012)","DOI":"10.1109\/ICST.2012.105"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Hierons, R.M., et al.: Using formal specifications to support testing. ACM Computing Surveys (2009)","DOI":"10.1145\/1459352.1459354"},{"key":"21_CR11","unstructured":"Zhao, Y., et al.: Modeling and verifying the code-level OSEK\/VDX operating system with CSP. In: 5th International Symposium on Theoretical Aspects of Software Engineering, pp. 142\u2013149 (2011)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"John, D.: OSEK\/VDX conformance testing - MODISTARC. In: Proceedings of OSEK\/VDX Open Systems in Automotive Networks (1998)","DOI":"10.1049\/ic:19981078"},{"key":"21_CR13","unstructured":"NuSMV: A New Symbolic Model Checking, http:\/\/nusmv.irst.itc.it\/"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Park, M., Byun, T., Choi, Y.: Property-based code slicing for efficient verification of osek\/vdx operating systems. In: First International Workshop on Formal Techniques for Safety-Critical Systems (2012)","DOI":"10.4204\/EPTCS.105.6"},{"key":"21_CR15","unstructured":"Tkachuk, O., Dwyer, M.B., Pasareanu, C.S.: Automated environment generation for software model checking. In: 18th IEEE International Conference on Automated Software Engineering, pp. 116\u2013129 (October 2003)"},{"key":"21_CR16","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.) SPIN 2010. LNCS, vol.\u00a06349, pp. 58\u201375. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40561-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,4]],"date-time":"2020-08-04T06:59:34Z","timestamp":1596524374000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40561-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405600","9783642405617"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40561-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}