{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T23:21:32Z","timestamp":1773789692291,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642342806","type":"print"},{"value":"9783642342813","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34281-3_17","type":"book-chapter","created":{"date-parts":[[2012,10,29]],"date-time":"2012-10-29T18:38:09Z","timestamp":1351535889000},"page":"214-229","source":"Crossref","is-referenced-by-count":5,"title":["Automatic Generation of Provably Correct Embedded Systems"],"prefix":"10.1007","author":[{"given":"Shang-Wei","family":"Lin","sequence":"first","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Pao-Ann","family":"Hsiung","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-540-40903-8_6","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T. Amnell","year":"2004","unstructured":"Amnell, T., Fersman, L., Mokrushin, E., Petterson, P., Yi, W.: TIMES: A Tool for Schedulability Analysis and Code Generation of Real-Time Systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 60\u201372. Springer, Heidelberg (2004)"},{"key":"17_CR2","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/BFb0028775","volume-title":"Computer Aided Verification","author":"C. Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R.: SCR*: A Toolset for Specifying and Analyzing Software Requirements. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 526\u2013531. Springer, Heidelberg (1998)"},{"issue":"4","key":"17_CR4","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.cl.2007.06.002","volume":"34","author":"P.A. Hsiung","year":"2008","unstructured":"Hsiung, P.A., Lin, S.W.: Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems. Computer Languages, Systems & Structures\u00a034(4), 153\u2013169 (2008)","journal-title":"Computer Languages, Systems & Structures"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-540-77092-3_62","volume-title":"Embedded and Ubiquitous Computing","author":"P.-A. Hsiung","year":"2007","unstructured":"Hsiung, P.-A., Lin, S.-W., Hung, C.-C., Fu, J.-M., Lin, C.-S., Chiang, C.-C., Chiang, K.-C., Lu, C.-H., Lu, P.-H.: Real-Time Embedded Software Design for Mobile and Ubiquitous Systems. In: Kuo, T.-W., Sha, E., Guo, M., Yang, L.T., Shao, Z. (eds.) EUC 2007. LNCS, vol.\u00a04808, pp. 718\u2013729. Springer, Heidelberg (2007)"},{"issue":"10","key":"17_CR6","doi-asserted-by":"publisher","first-page":"656","DOI":"10.1109\/TSE.2004.68","volume":"30","author":"P.A. Hsiung","year":"2004","unstructured":"Hsiung, P.A., Lin, S.W., Tseng, C.H., Lee, T.Y., Fu, J.M., See, W.B.: VERTAF: An application framework for the design and verification of embedded real-time software. IEEE Transactions on Software Engineering\u00a030(10), 656\u2013674 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45739-9_23","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A. Knapp","year":"2002","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model Checking - Timed UML State Machines and Collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 395\u2013414. Springer, Heidelberg (2002)"},{"key":"17_CR8","unstructured":"Lin, S.W.: https:\/\/sites.google.com\/site\/shangweilin\/pat-codegen"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-642-15643-4_30","volume-title":"Automated Technology for Verification and Analysis","author":"Y. Liu","year":"2010","unstructured":"Liu, Y., Sun, J., Dong, J.S.: Developing Model Checkers Using PAT. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol.\u00a06252, pp. 371\u2013377. Springer, Heidelberg (2010)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from event-B models. In: SoICT 2011, pp. 179\u2013188 (2011)","DOI":"10.1145\/2069216.2069252"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Niz, D., Rajkumar, R.: Time Weaver: A software-through-models framework for embedded real-time systems. In: LCTES, pp. 133\u2013143 (2003)","DOI":"10.1145\/780731.780751"},{"issue":"3","key":"17_CR12","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"10","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters\u00a010(3), 115\u2013116 (1981)","journal-title":"Information Processing Letters"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Ramkarthik, S., Zhang, C.: Generating java skeletal code with design contracts from specifications in a subset of object Z. In: ACIS-ICIS 2006, pp. 405\u2013411 (2006)","DOI":"10.1109\/ICIS-COMSAR.2006.41"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Samek, M.: Practical UML Statecharts in C\/C++: Event-Driven Programming for Embedded Systems. Newnes (2008)","DOI":"10.1201\/b16463"},{"key":"17_CR15","unstructured":"SCADE, http:\/\/www.esterel-technologies.com\/products\/scade-suite\/"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: TASE 2009, vol. 962, pp. 127\u2013135 (2009)","DOI":"10.1109\/TASE.2009.32"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Thompson, J.M., Heimdahl, M.P.E., Miller, S.P.: Specification-based prototyping for embedded systems. In: SIGSOFT 1999, pp. 163\u2013179 (1999)","DOI":"10.1007\/3-540-48166-4_11"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34281-3_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,19]],"date-time":"2025-04-19T21:24:34Z","timestamp":1745097874000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34281-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642342806","9783642342813"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34281-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}