{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T11:48:23Z","timestamp":1763466503332,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216898"},{"type":"electronic","value":"9783319216904"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_37","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T02:08:27Z","timestamp":1436926107000},"page":"536-543","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Meeting a Powertrain Verification Challenge"],"prefix":"10.1007","author":[{"given":"Parasara Sridhar","family":"Duggirala","sequence":"first","affiliation":[]},{"given":"Chuchu","family":"Fan","sequence":"additional","affiliation":[]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"issue":"3","key":"37_CR1","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1109\/9.989067","volume":"47","author":"D Angeli","year":"2000","unstructured":"Angeli, D.: A lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410\u2013421 (2000)","journal-title":"IEEE Trans. Autom. Control"},{"key":"37_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254\u2013257. Springer, Heidelberg (2011)"},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"key":"37_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010)"},{"key":"37_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-319-17524-9_10","volume-title":"NASA Formal Methods","author":"T Dreossi","year":"2015","unstructured":"Dreossi, T., Dang, T., Donz\u00e9, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127\u2013142. Springer, Heidelberg (2015)"},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: Proceedings of the International Conference on Embedded Software, EMSOFT 2013, pp. 1\u201310. IEEE (2013)","DOI":"10.1109\/EMSOFT.2013.6658604"},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-662-46681-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68\u201382. Springer, Heidelberg (2015)"},{"key":"37_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-06410-9_16","volume-title":"FM 2014: Formal Methods","author":"PS Duggirala","year":"2014","unstructured":"Duggirala, P.S., Wang, L., Mitra, S., Viswanathan, M., Mu\u00f1oz, C.: Temporal precedence checking for switched models and its application to a parallel landing protocol. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 215\u2013229. Springer, Heidelberg (2014)"},{"key":"37_CR9","unstructured":"Eigen, a C++ template library for linear algebra. \n                      http:\/\/eigen.tuxfamily.org\n                      \n                     Accessed Feb 2015"},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"Fan, C., Mitra, S.: Bounded verification using on-the-fly discrepancy computation. Technical report UILU-ENG-15-2201, Coordinated Science Laboratory. University of Illinois at Urbana-Champaign (2015)","DOI":"10.1007\/978-3-319-24953-7_32"},{"key":"37_CR11","unstructured":"Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Benchmarks for model transformations and conformance checking. In: 1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH) (2014)"},{"key":"37_CR12","doi-asserted-by":"crossref","unstructured":"Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: Proceedings of the 17th international conference on Hybrid systems: computation and control, pp. 253\u2013262. ACM (2014)","DOI":"10.1145\/2562059.2562140"},{"key":"37_CR13","doi-asserted-by":"crossref","unstructured":"Jin, X., Donz\u00e9, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: Proceedings of the 16th international conference on Hybrid systems: computation and control, pp. 43\u201352. ACM (2013)","DOI":"10.1145\/2461328.2461337"},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"Jin, X., Donz\u00e9, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: EEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2016, to appear)","DOI":"10.1109\/TCAD.2015.2421907"},{"issue":"4","key":"37_CR15","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1016\/S0005-1098(98)00019-3","volume":"36","author":"W Lohmiller","year":"1998","unstructured":"Lohmiller, W., Slotine, J.J.E.: On contraction analysis for non-linear systems. Automatica 36(4), 683\u2013696 (1998)","journal-title":"Automatica"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:10:41Z","timestamp":1563826241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_37","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":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}