{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T10:55:56Z","timestamp":1761562556954,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319919072"},{"type":"electronic","value":"9783319919089"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-319-91908-9_22","type":"book-chapter","created":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T05:05:00Z","timestamp":1570165500000},"page":"452-477","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Continuous-Time Models for System Design and Analysis"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Mirco","family":"Giacobbe","sequence":"additional","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Miku\u010dionis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,5]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-49382-2_22","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"L Aceto","year":"1998","unstructured":"Aceto, L., Bouyer, P., Burgue\u00f1o, A., Larsen, K.G.: The power of reachability testing for timed automata. In: Arvind, V., Ramanujam, S. (eds.) FSTTCS 1998. LNCS, vol. 1530, pp. 245\u2013256. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/978-3-540-49382-2_22"},{"key":"22_CR2","volume-title":"Principles of Cyber-Physical Systems","author":"R Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)"},{"issue":"1","key":"22_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"22_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"22_CR5","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. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"issue":"7","key":"22_CR6","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"issue":"2","key":"22_CR7","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1002\/spe.1006","volume":"41","author":"G Behrmann","year":"2011","unstructured":"Behrmann, G., David, A., Larsen, K., Pettersson, P., Yi, W.: Developing uppaal over 15 years. Softw. - Pract. Exp. 41(2), 133\u2013142 (2011)","journal-title":"Softw. - Pract. Exp."},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"22_CR9","volume-title":"Handbook of Model Checking","author":"P Bouyer","year":"2017","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Clarke, E., Henzinger, T., Veith, H. (eds.) Handbook of Model Checking. Springer, Heidelberg (2017)"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.ic.2014.01.014","volume":"236","author":"T Chen","year":"2014","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Inf. Comput. 236, 87\u2013101 (2014). Special Issue on Hybrid Systems and Biology","journal-title":"Inf. Comput."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. In: Proceedings of 19th ACM Symposium on Principles of Programming Languages, pp. 343\u2013354 (1992)","DOI":"10.1145\/143165.143235"},{"key":"22_CR12","volume-title":"Model Checking","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"issue":"1","key":"22_CR13","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1109\/JPROC.2011.2160929","volume":"100","author":"P Derler","year":"2012","unstructured":"Derler, P., Lee, E.A., Sangiovanni-Vincentelli, A.L.: Modeling cyber-physical systems. Proc. IEEE 100(1), 13\u201328 (2012)","journal-title":"Proc. IEEE"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/978-3-319-21690-4_37","volume-title":"Computer Aided Verification","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Fan, C., Mitra, S., Viswanathan, M.: Meeting a powertrain verification challenge. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 536\u2013543. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21690-4_37"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: IEEE American Control Conference, pp. 3567\u20133572 (2012)","DOI":"10.1109\/ACC.2012.6315384"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258\u2013273. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/978-3-540-31954-2_17"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11813040_1","volume-title":"FM 2006: Formal Methods","author":"TA Henzinger","year":"2006","unstructured":"Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 1\u201315. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11813040_1"},{"key":"22_CR19","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems, vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/978-3-642-59615-5_13"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460\u2013463. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/3-540-63166-6_48"},{"issue":"1","key":"22_CR21","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 188\u2013203. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-28756-5_14"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.: Quantitative verification: models, techniques, and tools. In: Proceedings of ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 449\u2013458 (2007)","DOI":"10.1145\/1287624.1287688"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-319-23506-6_17","volume-title":"Correct System Design","author":"KG Larsen","year":"2015","unstructured":"Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.: Safe and optimal adaptive cruise control. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 260\u2013277. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-23506-6_17"},{"issue":"1\u20132","key":"22_CR25","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. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"22_CR26","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/2.868693","volume":"33","author":"EA Lee","year":"2000","unstructured":"Lee, E.A.: What\u2019s ahead for embedded software. IEEE Comput. 33, 18\u201326 (2000)","journal-title":"IEEE Comput."},{"issue":"1","key":"22_CR27","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1109\/JPROC.2011.2165270","volume":"100","author":"I Lee","year":"2012","unstructured":"Lee, I., Sokolsky, O., Chen, S., Hatcliff, J., Jee, E., Kim, B., King, A., Mullen-Fortino, M., Park, S., Roederer, A., Venkatasubramanian, K.: Challenges and research directions in medical cyber-physical systems. Proc. IEEE 100(1), 75\u201390 (2012)","journal-title":"Proc. IEEE"},{"issue":"4","key":"22_CR28","first-page":"127:1","volume":"13","author":"M Pajic","year":"2014","unstructured":"Pajic, M., Jiang, Z., Lee, I., Sokolsky, O., Mangharam, R.: Safety-critical medical device development using the UPP2SF model translation tool. ACM Trans. Embed. Comput. Syst. 13(4), 127:1\u2013127:26 (2014)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"issue":"1","key":"22_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"22_CR30","unstructured":"Ye, P., Entcheva, E., Grosu, R., Smolka, S.A.: Efficient modeling of excitable cells using hybrid automata. In: Proceedings of Computational Methods in System Biology, pp. 216\u2013227 (2005)"}],"container-title":["Lecture Notes in Computer Science","Computing and Software Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91908-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T20:04:03Z","timestamp":1570305843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91908-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783319919072","9783319919089"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91908-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}