{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T15:24:02Z","timestamp":1766157842859,"version":"3.40.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175232"},{"type":"electronic","value":"9783319175249"}],"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-17524-9_18","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"248-262","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Verified ROS-Based Deployment of Platform-Independent Control Systems"],"prefix":"10.1007","author":[{"given":"Wenrui","family":"Meng","sequence":"first","affiliation":[]},{"given":"Junkil","family":"Park","sequence":"additional","affiliation":[]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Formal methods for the design of real-time systems, pp. 200\u2013236. Springer (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Halbwachs, N.: A synchronous language at work: the story of lustre. In: Formal Methods for Industrial Critical Systems: A Survey of Applications, pp. 15\u201331 (2005)","DOI":"10.1002\/9781118459898.ch2"},{"key":"18_CR3","unstructured":"Quigley, M., Conley, K., Gerkey, B., Faust, J., Foote, T., Leibs, J., Wheeler, R., Ng, A.Y.: ROS: an open-source robot operating system. In: ICRA workshop on open source software, vol. 3 (2009)"},{"key":"18_CR4","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal Project, Version 8.0. (2004)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Meng, W., Park, J., Sokolsky, O., Weirich, S., Lee, I.: Verified ros-based deployment of platform-independent control systems. In: University of Pennsylvania Department of Computer and Information Science Technical Report No. MS-MS-CIS-15-01, February 2015","DOI":"10.1007\/978-3-319-17524-9_18"},{"key":"18_CR7","unstructured":"Leroy, X.: The compcert c verified compiler (2012)"},{"key":"18_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., Robert, D., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press, UK (2014)"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Pajic, M., Bezzo, N., Weimer, J., Sokolsky, O., Michael, N., Pappas, G.J., Tabuada, P., Lee, I.: Demo abstract: Synthesis of platform-aware attack-resilient vehicular systems. In: Cyber-Physical Systems (ICCPS), 2013 ACM\/IEEE International Conference on, pp. 251\u2013251. IEEE (2013)","DOI":"10.1145\/2502524.2502570"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-01924-1_17","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2009","author":"G Lasnier","year":"2009","unstructured":"Lasnier, G., Zalila, B., Pautet, L., Hugues, J.: Ocarina: an environment for AADL models analysis and automatic code generation for high integrity applications. In: Kordon, F., Kermarrec, Y. (eds.) Ada-Europe 2009. LNCS, vol. 5570, pp. 237\u2013250. Springer, Heidelberg (2009)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Kim, B.G., Phan, L.T.X., Sokolsky, O., Lee, I.: Platform-dependent code generation for embedded real-time software. In: Compilers, Architecture and Synthesis for Embedded Systems (CASES), 2013 International Conference on, pp. 1\u201310. IEEE (2013)","DOI":"10.1109\/CASES.2013.6662512"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Narayanan, A., Karsai, G.: Towards verifying model transformations. In: Proceedings of the 5$$^{th}$$ International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2006), pp. 191\u2013200 (2008)","DOI":"10.1016\/j.entcs.2008.04.041"},{"issue":"2","key":"18_CR13","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/j.jss.2009.08.012","volume":"83","author":"J Cabot","year":"2010","unstructured":"Cabot, J., Claris\u00f3, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. Journal of Systems and Software 83(2), 283\u2013302 (2010)","journal-title":"Journal of Systems and Software"},{"key":"18_CR14","unstructured":"Lucio, L., Vangheluwe, H.: Model transformations to verify model transformations. In: Proceedings of the Workshop on Verification of Model Transformations, June 2013"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T07:29:13Z","timestamp":1676446153000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}