{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T03:41:17Z","timestamp":1743046877506,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319929699"},{"type":"electronic","value":"9783319929705"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-92970-5_16","type":"book-chapter","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T08:54:12Z","timestamp":1527584052000},"page":"254-268","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated Validation of IoT Device Control Programs Through Domain-Specific Model Generation"],"prefix":"10.1007","author":[{"given":"Yunja","family":"Choi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,30]]},"reference":[{"key":"16_CR1","unstructured":"Erika realtime operating system. http:\/\/erika.tuxfamily.org\/drupal\/"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Artho, C., Gros, Q., Rousset, G., Banzai, K., Ma, L., Kitamura, T., Hagiya, M., Tanabe, Y., Yamamoto, M.: Model-based API Testing of Apache ZooKeeper. In: Proceedings of 10th IEEE International Conference on Software Testing, Verification and Validation, pp. 288\u2013298 (2017)","DOI":"10.1109\/ICST.2017.33"},{"key":"16_CR3","unstructured":"Berry, G.: Synchronous design and verification of critical embedded systems using SCADE and Esterel. In: 12th International Conference on Formal Methods for Industrial Critical Systems (2007)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bucur, D., Kwiatowska, M.Z.: Poster abstract: software verification for TinyOS. In: 9th ACM\/IEEE International Conference on Information Processing in Sensor Networks (2010)","DOI":"10.1145\/1791212.1791274"},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1016\/j.jss.2017.07.040","volume":"137","author":"Y Choi","year":"2018","unstructured":"Choi, Y.: A configurable V&V framework using formal behavioral patterns for automotive control software. J. Syst. Softw. 137, 563\u2013579 (2018)","journal-title":"J. Syst. Softw."},{"issue":"1","key":"16_CR6","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s10270-014-0449-6","volume":"16","author":"Y Choi","year":"2017","unstructured":"Choi, Y., Byun, T.: Constraint-based test generation for automotive operating systems. Softw. Syst. Model. 16(1), 7\u201324 (2017)","journal-title":"Softw. Syst. Model."},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Chung, Y., Kim, D., Choi, Y.: Modeling OSEK\/VDX OS requirements in C. In: 24th Asia-Pacific Software Engineering Conference (2017)","DOI":"10.1109\/APSEC.2017.46"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Chen, H., Marques-Silva, J.: Semiformal verification of embedded software in medical devices considering stringent hardware constraints. In: International Conference on Embedded Software and Systems (2009)","DOI":"10.1109\/ICESS.2009.82"},{"issue":"4","key":"16_CR10","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957\u2013974 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"DuVarney, D.C., Purushothaman Iyer, S., Wolf, C.: A toolset for extracting models from C programs. In: 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, pp. 260\u2013275 (2002)","DOI":"10.1007\/3-540-36135-9_17"},{"key":"16_CR12","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1016\/j.scico.2011.10.003","volume":"77","author":"MM Gallardo","year":"2012","unstructured":"Gallardo, M.M., Joubert, C., Merino, P., Sanan, D.: A model-extraction approach to verifying concurrent C programs with CADP. Sci. Comput. Program. 77, 375\u2013392 (2012)","journal-title":"Sci. Comput. Program."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Gong, X., Ma, J., Li, Q., Zhang, J.: Automatic model building and verification of embedded software with UPPAAL. In: International Joint Conference of IEEE TrustCom\/IEEE ICESS\/FCST, pp. 1118\u20131124 (2011)","DOI":"10.1109\/TrustCom.2011.152"},{"key":"16_CR14","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/s10270-007-0077-5","volume":"7","author":"S Graf","year":"2008","unstructured":"Graf, S.: OMEGA: correct development of real time and embedded systems. Softw. Syst. Model. 7, 127\u2013130 (2008)","journal-title":"Softw. Syst. Model."},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Hili, N., Dingel, J., Beaulieu, A.: Modelling and code generation for real-time embedded systems with UML-RT and Papyrus-RT. In: IEEE 39th International Conference on Software Engineering Companion (2017)","DOI":"10.1109\/ICSE-C.2017.168"},{"issue":"8","key":"16_CR16","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"16_CR17","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Publishing Company, Reading (2003)"},{"key":"16_CR18","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s10515-008-0033-9","volume":"15","author":"GJ Holzmann","year":"2008","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Model driven code checking. Automa. Softw. Eng. 15, 283\u2013297 (2008)","journal-title":"Automa. Softw. Eng."},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/11537328_3","volume-title":"Model Checking Software","author":"GJ Holzmann","year":"2005","unstructured":"Holzmann, G.J., Ruys, T.C.: Effective bug hunting with Spin and Modex. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, p. 24. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11537328_3"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Ichii, M., Myojin, T., Nakagawa, Y.: A rule-based automated approach for extracting models from source code. In: 19th Working Conference on Reverse Engineering, pp. 308\u2013317 (2012)","DOI":"10.1109\/WCRE.2012.40"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Kim, Y., Kim, M.: SAT-based bounded software model checking for embedded software: a case study. In: 21st Asia-Pacific Software Engineering Conference, pp. 737\u2013748 (2014)","DOI":"10.1109\/APSEC.2014.17"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Matinnejad, R., Nejati, S., Briand, L.C., Bruckmann, T.: Automated test suite generation for time-continuous simulink models. In: IEEE\/ACM 38th International Conference on Software Engineering, pp. 595\u2013606 (2016)","DOI":"10.1145\/2884781.2884797"},{"key":"16_CR23","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1007\/s00165-017-0419-1","volume":"29","author":"P Schrammel","year":"2017","unstructured":"Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienmueller, T.: Incremental bounded model checking for embedded software. Formal Aspects Comput. 29, 911\u2013931 (2017)","journal-title":"Formal Aspects Comput."},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Wu, X., Wen, Y., Chen, L., Dong, W., Wang, J.: Data race detection for interrupt-driven programs via bounded model checking. In: IEEE 7th International Conference on Software Security and Reliability Companion, pp. 204\u2013210 (2013)","DOI":"10.1109\/SERE-C.2013.33"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Zhang, H., Aoki, T., Chiba, Y.: Yes! you can use your model checker to verify OSEK\/VDX applications. In: IEEE 8th International Conference on Software Testing, Verification, and Validation (2015)","DOI":"10.1109\/ICST.2015.7102612"}],"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-319-92970-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T15:24:04Z","timestamp":1571412244000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92970-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929699","9783319929705"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92970-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}