{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:43:46Z","timestamp":1761648226405,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319121536"},{"type":"electronic","value":"9783319121543"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_16","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"252-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Timed Refinement for Verification of Real-Time Object Code Programs"],"prefix":"10.1007","author":[{"given":"Mohana Asha Latha","family":"Dubasi","sequence":"first","affiliation":[]},{"given":"Sudarshan K.","family":"Srinivasan","sequence":"additional","affiliation":[]},{"given":"Vidura","family":"Wijayasekara","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/BFb0015008","volume-title":"CONCUR \u201994: Concurrency Theory","author":"R Alur","year":"1994","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 162\u2013177. Springer, Heidelberg (1994)"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Boudjadar, A., Bodeveix, J.-P., Filali, M.: Compositional refinement for real-time systems with priorities. In: Moszkowski, B.C., Reynolds, M., Terenziani, P. (eds.) TIME, pp. 57\u201364. IEEE Computer Society (2012)","DOI":"10.1109\/TIME.2012.21"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0055357","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: KRONOS: a model-checking tool for real-time systems (Tool-presentation for FTRTFT \u201998). In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 298\u2013302. Springer, Heidelberg (1998)"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I\/O automata: a complete specification theory for real-time systems. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 91\u2013100. ACM (2010)","DOI":"10.1145\/1755952.1755967"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Godskesen, J.C., Larsen, K.G., Skou, A.: Automatic verification of real-time systems using epsilon. In: Vuong, S.T., Chanson, S.T. (eds.) PSTV. vol. 1, IFIP Conference Proceedings, pp. 323\u2013330. Chapman & Hall (1994)","DOI":"10.1007\/978-0-387-34867-4_21"},{"key":"16_CR7","unstructured":"Keil Cortex-M Evaluation Board Comparison, November 2013. http:\/\/www.keil.com\/arm\/boards\/cortexm.asp"},{"key":"16_CR8","volume-title":"Industrial Electronics","author":"TE Kissell","year":"2006","unstructured":"Kissell, T.E.: Industrial Electronics. Prentice Hall, New Delhi (2006)"},{"issue":"1\u20132","key":"16_CR9","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1(1\u20132), 134\u2013152 (1997)","journal-title":"STTT"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-40922-X_11","volume-title":"Formal Methods in Computer-Aided Design","author":"P Manolios","year":"2000","unstructured":"Manolios, P.: Correctness of pipelined machines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 161\u2013178. Springer, Heidelberg (2000)"},{"key":"16_CR11","unstructured":"Manolios, P.: Mechanical verification of reactive systems. Ph.D. thesis, University of Texas at Austin, August 2001. http:\/\/www.ccs.neu.edu\/home\/pete\/research\/phd-dissertation.html"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-39724-3_28","volume-title":"Correct Hardware Design and Verification Methods","author":"P Manolios","year":"2003","unstructured":"Manolios, P.: A compositional theory of refinement for branching time. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 304\u2013318. Springer, Heidelberg (2003)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-73368-3_35","volume-title":"Computer Aided Verification","author":"P Manolios","year":"2007","unstructured":"Manolios, P., Srinivasan, S.K., Vroon, D.: BAT: the bit-level analysis tool. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 303\u2013306. Springer, Heidelberg (2007)"},{"key":"16_CR14","unstructured":"List of Device Recalls, U.S. Food and Drug Admin, July 2010"},{"issue":"3","key":"16_CR15","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/s10817-012-9258-1","volume":"51","author":"S Ray","year":"2013","unstructured":"Ray, S., Sumners, R.: Specification and verification of concurrent programs through refinements. J. Autom. Reasoning 51(3), 241\u2013280 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR16","unstructured":"Sandler, K., Ohrstrom, L., Moy, L., McVay, R.: Killed by Code: Software Transparency in Implantable Medical Devices. Software Freedom Law Center (2010)"},{"key":"16_CR17","unstructured":"The Satisfiability Modulo Theories Library, November 2013. http:\/\/www.smtlib.org\/"},{"key":"16_CR18","unstructured":"Stepper Motors, January 2014. http:\/\/www.telcointercon.com\/stepper-motors-10.html"},{"key":"16_CR19","unstructured":"Toyota Seeks a Settlement for Sudden Acceleration Cases, December 2013. http:\/\/www.nytimes.com\/2013\/12\/14\/business\/toyota-seeks-settlement-for-lawsuits.html?_r=0"},{"issue":"3","key":"16_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1347375.1347389","volume":"7","author":"R Wilhelm","year":"2008","unstructured":"Wilhelm, R., Engblom, J.: The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7(3), 1\u201353 (2008)","journal-title":"ACM Trans. Embedded Comput. Syst."},{"key":"16_CR21","unstructured":"z3, November 2013. http:\/\/z3.codeplex.com\/"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12154-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T14:44:34Z","timestamp":1676904274000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}