{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T11:10:07Z","timestamp":1744024207455,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642329425"},{"type":"electronic","value":"9783642329432"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32943-2_15","type":"book-chapter","created":{"date-parts":[[2012,8,28]],"date-time":"2012-08-28T04:59:35Z","timestamp":1346129975000},"page":"183-197","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking of OSEK\/VDX OS Design Model Based on Environment Modeling"],"prefix":"10.1007","author":[{"given":"Kenro","family":"Yatake","sequence":"first","affiliation":[]},{"given":"Toshiaki","family":"Aoki","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Yices: An SMT Solver, http:\/\/yices.csl.sri.com\/"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Aoki, T.: Model Checking Multi-Task Software on Real-Time Operating Systems. In: ISORC, pp. 551\u2013555. IEEE Computer Society (2008)","DOI":"10.1109\/ISORC.2008.46"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1109\/ICSTW.2008.54","volume-title":"Proceedings of the 2008 IEEE International Conference on Software Testing Verification and Validation Workshop","author":"J. Cabot","year":"2008","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verification of UML\/OCL Class Diagrams using Constraint Programming. In: Proceedings of the 2008 IEEE International Conference on Software Testing Verification and Validation Workshop, pp. 73\u201380. IEEE Computer Society, Washington, DC (2008)"},{"key":"15_CR4","unstructured":"Clavel, M., Egea, M., de Dios, M.A.G.: Checking Unsatisfiability for OCL Constraints. ECEASST\u00a024 (2009)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-642-04425-0_34","volume-title":"Model Driven Engineering Languages and Systems","author":"P. Dhaussy","year":"2009","unstructured":"Dhaussy, P., Pillain, P.-Y., Creff, S., Raji, A., Le Traon, Y., Baudry, B.: Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol.\u00a05795, pp. 438\u2013452. Springer, Heidelberg (2009)"},{"key":"15_CR6","unstructured":"Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley (2004)"},{"key":"15_CR7","unstructured":"OMG. Unified Modeling Language (1989), http:\/\/www.uml.org\/"},{"key":"15_CR8","unstructured":"OSEK\/VDX. OSEK\/VDX Operating System Specification 2.2.3 (2005), http:\/\/portal.osek-vdx.org\/"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Parizek, P., Plasil, F.: Partial Verification of Software Components: Heuristics for Environment Construction. In: EUROMICRO-SEAA, pp. 75\u201382. IEEE Computer Society (2007)","DOI":"10.1109\/EUROMICRO.2007.46"},{"key":"15_CR10","unstructured":"Pasareanu, C.S.: DEOS Kernel: Environment Modeling using LTL Assumptions. Nasa ames technical report nasa-arc-ic-2000-196, NASA Ames Research Center (2000)"},{"issue":"2","key":"15_CR11","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s10703-005-1490-4","volume":"26","author":"J. Penix","year":"2005","unstructured":"Penix, J., Visser, W., Park, S., Pasareanu, C.S., Engstrom, E., Larson, A., Weininger, N.: Verifying Time Partitioning in the DEOS Scheduling Kernel. Formal Methods in System Design\u00a026(2), 103\u2013135 (2005)","journal-title":"Formal Methods in System Design"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Rajan, S.P., Tkachuk, O., Prasad, M.R., Ghosh, I., Goel, N., Uehara, T.: WEAVE: WEb Applications Validation Environment. In: ICSE Companion, pp. 101\u2013111. IEEE (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5070968"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Raji, A., Dhaussy, P.: Use Cases Modeling for Scalable Model-Checking. In: APSEC 2011, Minh City, Viet Nam (December 2011)","DOI":"10.1109\/APSEC.2011.25"},{"issue":"3","key":"15_CR14","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1049\/iet-sen.2009.0017","volume":"4","author":"O. Tkachuk","year":"2010","unstructured":"Tkachuk, O., Dwyer, M.B.: Environment generation for validating event-driven software using model checking. IET Software\u00a04(3), 194\u2013209 (2010)","journal-title":"IET Software"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M.B., Pasareanu, C.S.: Automated Environment Generation for Software Model Checking. In: ASE, pp. 116\u2013129. IEEE Computer Society (2003)","DOI":"10.1109\/ASE.2003.1240300"},{"key":"15_CR16","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley (1999)"},{"key":"15_CR17","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","Theoretical Aspects of Computing \u2013 ICTAC 2012"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32943-2_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T10:33:47Z","timestamp":1744022027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32943-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642329425","9783642329432"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32943-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}