{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T08:54:02Z","timestamp":1781254442647,"version":"3.54.1"},"publisher-location":"Cham","reference-count":132,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319756318","type":"print"},{"value":"9783319756325","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-75632-5_5","type":"book-chapter","created":{"date-parts":[[2018,2,10]],"date-time":"2018-02-10T01:09:21Z","timestamp":1518224961000},"page":"135-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":248,"title":["Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications"],"prefix":"10.1007","author":[{"given":"Ezio","family":"Bartocci","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jyotirmoy","family":"Deshmukh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexandre","family":"Donz\u00e9","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dejan","family":"Ni\u010dkovi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,2,11]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abbas, H., Fainekos, G.: Computing descent direction of MTL robustness for non-linear systems. In: Proceedings of ACC 2013: The 2013 American Control Conference, pp. 4405\u20134410 (2013)","DOI":"10.1109\/ACC.2013.6580518"},{"issue":"s2","key":"5_CR2","first-page":"95:1","volume":"12","author":"H Abbas","year":"2013","unstructured":"Abbas, H., Fainekos, G.E., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 12(s2), 95:1\u201395:30 (2013)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Abbas, H., Hoxha, B., Fainekos, G., Ueda, K.: Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems. In: Proceedings of the 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent, pp. 1\u20136. IEEE (2014)","DOI":"10.1109\/CYBER.2014.6917426"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Abbas, H., Mittelmann, H., Fainekos, G.E.: Formal property verification in a conformance testing framework. In: Proceedings of MEMOCODE 2014: The 12th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 155\u2013164. IEEE (2014)","DOI":"10.1109\/MEMCOD.2014.6961854"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-67471-1_2","volume-title":"Computational Methods in Systems Biology","author":"H Abbas","year":"2017","unstructured":"Abbas, H., Rodionova, A., Bartocci, E., Smolka, S.A., Grosu, R.: Quantitative regular expressions for Arrhythmia detection algorithms. In: Feret, J., Koeppl, H. (eds.) CMSB 2017. LNCS, vol. 10545, pp. 23\u201339. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67471-1_2"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Abbas, H., Winn, A., Fainekos, G.E., Julius, A.A.: Functional gradient descent method for metric temporal logic specifications. In: Proceedings of ACC 2014: The American Control Conference, pp. 2312\u20132317. IEEE (2014)","DOI":"10.1109\/ACC.2014.6859453"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-319-21668-3_21","volume-title":"Computer Aided Verification","author":"T Akazaki","year":"2015","unstructured":"Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 356\u2013374. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_21"},{"issue":"1","key":"5_CR8","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Annapureddy, Y.S.R., Fainekos, G.E.: Ant colonies for temporal logic falsification of hybrid systems. In: Proceedings of IECON 2010: The 36th Annual Conference on IEEE Industrial Electronics Society, pp. 91\u201396 (2010)","DOI":"10.1109\/IECON.2010.5675195"},{"key":"5_CR10","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). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21"},{"issue":"2","key":"5_CR11","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1145\/506147.506151","volume":"49","author":"E Asarin","year":"2002","unstructured":"Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172\u2013206 (2002)","journal-title":"J. ACM"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Aydin-Gol, E., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: Proceedings of CDC 2014: The 53rd IEEE Conference on Decision and Control, pp. 108\u2013113. IEEE (2014)","DOI":"10.1109\/CDC.2014.7039367"},{"issue":"99","key":"5_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/TCNS.2016.2609138","volume":"PP","author":"E Bartocci","year":"2016","unstructured":"Bartocci, E., Aydin-Gol, E., Haghighi, I., Belta, C.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans. Control Netw. Syst. PP(99), 1\u201312 (2016)","journal-title":"IEEE Trans. Control Netw. Syst."},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-11164-3_1","volume-title":"Runtime Verification","author":"E Bartocci","year":"2014","unstructured":"Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 1\u20139. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_1"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Proceedings of MEMOCODE 2017: The 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 146\u2013155. ACM (2017)","DOI":"10.1145\/3127041.3127050"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-26916-0_9","volume-title":"Hybrid Systems Biology","author":"E Bartocci","year":"2015","unstructured":"Bartocci, E., Bortolussi, L., Milios, D., Nenzi, L., Sanguinetti, G.: Studying emergent behaviours in morphogenesis using signal spatio-temporal logic. In: Abate, A., \u0160afr\u00e1nek, D. (eds.) HSB 2015. LNCS, vol. 9271, pp. 156\u2013172. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26916-0_9"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-40708-6_13","volume-title":"Computational Methods in Systems Biology","author":"E Bartocci","year":"2013","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 164\u2013177. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40708-6_13"},{"key":"5_CR18","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.tcs.2015.02.046","volume":"587","author":"E Bartocci","year":"2015","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587, 3\u201325 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-10512-3_3","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"E Bartocci","year":"2014","unstructured":"Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 23\u201337. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10512-3_3"},{"issue":"33\u201334","key":"5_CR20","doi-asserted-by":"crossref","first-page":"3149","DOI":"10.1016\/j.tcs.2009.02.042","volume":"410","author":"E Bartocci","year":"2009","unstructured":"Bartocci, E., Corradini, F., Berardini, M.R.D., Entcheva, E., Smolka, S.A., Grosu, R.: Modeling and simulation of cardiac tissue using hybrid I\/O automata. Theor. Comput. Sci. 410(33\u201334), 3149\u20133165 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"5_CR21","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.entcs.2009.02.004","volume":"229","author":"E Bartocci","year":"2009","unstructured":"Bartocci, E., Corradini, F., Merelli, E., Tesei, L.: Model checking biological oscillators. Electr. Notes Theor. Comput. Sci. 229(1), 41\u201358 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"20","key":"5_CR22","doi-asserted-by":"crossref","first-page":"1999","DOI":"10.1016\/j.tcs.2009.12.019","volume":"411","author":"E Bartocci","year":"2010","unstructured":"Bartocci, E., Corradini, F., Merelli, E., Tesei, L.: Detecting synchronisation of biological oscillators by model checking. Theor. Comput. Sci. 411(20), 1999\u20132018 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transf., 1\u201340, April 2017","DOI":"10.1007\/s10009-017-0454-5"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-35632-2_18","volume-title":"Runtime Verification","author":"E Bartocci","year":"2013","unstructured":"Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 168\u2013182. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_18"},{"issue":"1","key":"5_CR25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1371\/journal.pcbi.1004591","volume":"12","author":"E Bartocci","year":"2016","unstructured":"Bartocci, E., Li\u00f2, P.: Computational modeling, formal analysis, and tools for systems biology. PLoS Comput. Biol. 12(1), 1\u201322 (2016)","journal-title":"PLoS Comput. Biol."},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-11164-3_4","volume-title":"Runtime Verification","author":"D Basin","year":"2014","unstructured":"Basin, D., Caronni, G., Ereth, S., Harvan, M., Klaedtke, F., Mantel, H.: Scalable offline monitoring. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 31\u201347. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_4"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-29860-8_27","volume-title":"Runtime Verification","author":"D Basin","year":"2012","unstructured":"Basin, D., Harvan, M., Klaedtke, F., Z\u0103linescu, E.: MONPOLY: monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 360\u2013364. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_27"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-40787-1_4","volume-title":"Runtime Verification","author":"A Bauer","year":"2013","unstructured":"Bauer, A., K\u00fcster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59\u201375. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_4"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11944836_25","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"A Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260\u2013272. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11944836_25"},{"issue":"3","key":"5_CR30","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Logic Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Logic Comput."},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-319-22264-6_6","volume-title":"Quantitative Evaluation of Systems","author":"L Bortolussi","year":"2015","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: U-check: model checking and parameter synthesis under uncertainty. In: Campos, J., Haverkort, B.R. (eds.) QEST 2015. LNCS, vol. 9259, pp. 89\u2013104. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22264-6_6"},{"key":"5_CR32","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.ic.2014.01.012","volume":"236","author":"L Brim","year":"2014","unstructured":"Brim, L., Dluhos, P., Safr\u00e1nek, D., Vejpustek, T.: STL $${}^{*}$$ \u2217 : Extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52\u201367 (2014)","journal-title":"Inf. Comput."},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Brim, L., Vejpustek, T., Safr\u00e1nek, D., Fabrikov\u00e1, J.: Robustness analysis for value-freezing signal temporal logic. In: Proceedings of HSB 2013: The Second International Workshop on Hybrid Systems and Biology. EPTCS, vol. 125, pp. 20\u201336 (2013)","DOI":"10.4204\/EPTCS.125.2"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-662-45231-8_30","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications","author":"S Bufo","year":"2014","unstructured":"Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 391\u2013403. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-45231-8_30"},{"issue":"5","key":"5_CR35","doi-asserted-by":"crossref","first-page":"1142","DOI":"10.1177\/193229681200600519","volume":"6","author":"F Cameron","year":"2012","unstructured":"Cameron, F., Wilson, D.M., Buckingham, B.A., Arzumanyan, H., Clinton, P., Chase, H.P., Lum, J., Maahs, D.M., Calhoun, P.M., Bequette, B.W.: Inpatient studies of a Kalman-filter-based predictive pump shutoff algorithm. J. Diabetes Sci. Technol. 6(5), 1142\u20131147 (2012)","journal-title":"J. Diabetes Sci. Technol."},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-23820-3_1","volume-title":"Runtime Verification","author":"F Cameron","year":"2015","unstructured":"Cameron, F., Fainekos, G., Maahs, D.M., Sankaranarayanan, S.: Towards a verified artificial pancreas: challenges and solutions for runtime verification. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 3\u201317. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_1"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-642-29860-8_22","volume-title":"Runtime Verification","author":"A Chakarov","year":"2012","unstructured":"Chakarov, A., Sankaranarayanan, S., Fainekos, G.: Combining time and frequency domain specifications for periodic signals. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 294\u2013309. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_22"},{"key":"5_CR38","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/RBME.2009.2036073","volume":"2","author":"C Cobelli","year":"2009","unstructured":"Cobelli, C., Man, C.D., Sparacino, G., Magni, L., Nicolao, G.D., Kovatchev, B.P.: Diabetes: Models, signals and control (methodological review). IEEE Rev. Biomed. Eng. 2, 54\u201395 (2009)","journal-title":"IEEE Rev. Biomed. Eng."},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: Proceedings of TIME 2005: The 12th International Symposium on Temporal Representation and Reasoning, pp. 166\u2013174. IEEE (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"5_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-23820-3_4","volume-title":"Runtime Verification","author":"JV Deshmukh","year":"2015","unstructured":"Deshmukh, J.V., Donz\u00e9, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 55\u201370. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_4"},{"issue":"1","key":"5_CR41","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10703-017-0286-7","volume":"51","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh, J.V., Donz\u00e9, A., Ghosh, S., Jin, X., Garvit, J., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Methods Syst. Des. 51(1), 5\u201330 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-319-21668-3_14","volume-title":"Computer Aided Verification","author":"JV Deshmukh","year":"2015","unstructured":"Deshmukh, J.V., Majumdar, R., Prabhu, V.S.: Quantifying conformance using the Skorokhod metric. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 234\u2013250. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_14"},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-11164-3_19","volume-title":"Runtime Verification","author":"A Dokhanchi","year":"2014","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231\u2013246. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_19"},{"key":"5_CR44","doi-asserted-by":"crossref","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.E.: Metric interval temporal logic specification elicitation and debugging. In: Proceedings of MEMOCODE 2015: The 13th ACM\/IEEE International Conference on Formal Methods and Models for Codesign, pp. 70\u201379. IEEE (2015)","DOI":"10.1109\/MEMCOD.2015.7340472"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Dokhanchi, A., Zutshi, A., Sriniva, R.T., Sankaranarayanan, S., Fainekos, G.: Requirements driven falsification with coverage metrics. In: Proceedings of EMSOFT: The 12th International Conference on Embedded Software, pp. 31\u201340. IEEE (2015)","DOI":"10.1109\/EMSOFT.2015.7318257"},{"key":"5_CR46","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). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_17"},{"key":"5_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-02008-7_11","volume-title":"Research in Computational Molecular Biology","author":"A Donz\u00e9","year":"2009","unstructured":"Donz\u00e9, A., Clermont, G., Legay, A., Langmead, C.J.: Parameter synthesis in nonlinear dynamical systems: application to systems biology. In: Batzoglou, S. (ed.) RECOMB 2009. LNCS, vol. 5541, pp. 155\u2013169. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02008-7_11"},{"key":"5_CR48","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Fanchon, E., Gattepaille, L.M., Maler, O., Tracqui, P.: Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE 6(9), e24246 (2011)","DOI":"10.1371\/journal.pone.0024246"},{"key":"5_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-39799-8_19","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264\u2013279. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19"},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-00602-9_12","volume-title":"Hybrid Systems: Computation and Control","author":"A Donz\u00e9","year":"2009","unstructured":"Donz\u00e9, A., Krogh, B., Rajhans, A.: Parameter synthesis for hybrid systems with an application to simulink models. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 165\u2013179. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00602-9_12"},{"key":"5_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9"},{"key":"5_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-33386-6_9","volume-title":"Automated Technology for Verification and Analysis","author":"A Donz\u00e9","year":"2012","unstructured":"Donz\u00e9, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 92\u2013106. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_9"},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_10"},{"key":"5_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-45069-6_11","volume-title":"Computer Aided Verification","author":"D Drusinsky","year":"2003","unstructured":"Drusinsky, D.: Monitoring temporal rules combined with time series. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 114\u2013117. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_11"},{"key":"5_CR55","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-36123-9","volume-title":"A Practical Introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/978-0-387-36123-9"},{"key":"5_CR56","doi-asserted-by":"crossref","unstructured":"Eisner, C., Fisman, D., Havlicek, J.: A topological characterization of weakness. In: Proceedings of PODC 2005: The 24th Annual ACM Symposium on Principles of Distributed Computing, pp. 1\u20138. ACM (2005)","DOI":"10.1145\/1073814.1073816"},{"key":"5_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27\u201339. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_3"},{"issue":"1","key":"5_CR58","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1080\/1068276031000074288","volume":"11","author":"GE Fainekos","year":"2003","unstructured":"Fainekos, G.E., Giannakoglou, K.C.: Inverse design of airfoils based on a novel formulation of the ant colony optimization method. Inverse Prob. Eng. 11(1), 21\u201338 (2003)","journal-title":"Inverse Prob. Eng."},{"key":"5_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/11867340_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"GE Fainekos","year":"2006","unstructured":"Fainekos, G.E., Girard, A., Pappas, G.J.: Temporal logic verification using simulation. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 171\u2013186. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11867340_13"},{"key":"5_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/11940197_12","volume-title":"Formal Approaches to Software Testing and Runtime Verification","author":"GE Fainekos","year":"2006","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications. In: Havelund, K., N\u00fa\u00f1ez, M., Ro\u015fu, G., Wolff, B. (eds.) FATES\/RV 2006. LNCS, vol. 4262, pp. 178\u2013192. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11940197_12"},{"issue":"42","key":"5_CR61","doi-asserted-by":"crossref","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR62","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: Proceedings of ACC 2012: The 2012 American Control Conference, pp. 3567\u20133572. IEEE (2012)","DOI":"10.1109\/ACC.2012.6315384"},{"key":"5_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-23820-3_27","volume-title":"Runtime Verification","author":"Y Falcone","year":"2015","unstructured":"Falcone, Y., Ni\u010dkovi\u0107, D., Reger, G., Thoma, D.: Second international competition on runtime verification. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 405\u2013422. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_27"},{"key":"5_CR64","unstructured":"Ferr\u00e8re, T.: Assertions and measurements for mixed-signal simulation. Ph.D. thesis. Universit\u00e9 Grenoble-Alpes, France (2016)"},{"key":"5_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-319-21668-3_19","volume-title":"Computer Aided Verification","author":"T Ferr\u00e8re","year":"2015","unstructured":"Ferr\u00e8re, T., Maler, O., Ni\u010dkovi\u0107, D., Ulus, D.: Measuring with timed patterns. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 322\u2013337. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_19"},{"issue":"2","key":"5_CR66","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/B:FORM.0000017718.28096.48","volume":"24","author":"B Finkbeiner","year":"2004","unstructured":"Finkbeiner, B., Sipma, H.B.: Checking finite traces using alternating automata. Formal Methods Syst. Des. 24(2), 101\u2013127 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","volume-title":"Computer Aided Verification","author":"R Grosu","year":"2011","unstructured":"Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396\u2013411. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_31"},{"issue":"3","key":"5_CR68","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1467247.1467271","volume":"52","author":"R Grosu","year":"2009","unstructured":"Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97\u2013105 (2009)","journal-title":"Commun. ACM"},{"key":"5_CR69","doi-asserted-by":"crossref","unstructured":"Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of HSCC 2015: The 18th International Conference on Hybrid Systems: Computation and Control, pp. 189\u2013198. IEEE (2015)","DOI":"10.1145\/2728606.2728633"},{"issue":"2","key":"5_CR70","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1016\/S1571-0661(04)00253-1","volume":"55","author":"K Havelund","year":"2001","unstructured":"Havelund, K., Rosu, G.: Monitoring Java programs with Java pathexplorer. Electron. Not. Theoret. Comput. Sci. 55(2), 200\u2013217 (2001)","journal-title":"Electron. Not. Theoret. Comput. Sci."},{"key":"5_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-11164-3_15","volume-title":"Runtime Verification","author":"H-M Ho","year":"2014","unstructured":"Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178\u2013192. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_15"},{"issue":"1","key":"5_CR72","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1111\/j.1464-5491.2005.01672.x","volume":"23","author":"R Hovorka","year":"2005","unstructured":"Hovorka, R.: Continuous glucose monitoring and closed-loop systems. Diabet. Med. 23(1), 1\u201312 (2005)","journal-title":"Diabet. Med."},{"key":"5_CR73","unstructured":"Hoxha, B., Bach, H., Abbas, H., Dokhanci, A., Kobayashi, Y., Fainekos, G.: Towards formal specification visualization for testing and monitoring of cyber-physical systems. In: International Workshop on Design and Implementation of Formal Tools and Systems, DIFTS 2014 (2014)"},{"key":"5_CR74","doi-asserted-by":"crossref","unstructured":"Hoxha, B., Dokhanchi, A., Fainekos, G.: Mining parametric temporal logic properties in model based design for cyber-physical systems. Int. J. Softw. Tools Technol. Transf. (2017). (in press)","DOI":"10.1007\/s10009-017-0447-4"},{"key":"5_CR75","doi-asserted-by":"crossref","unstructured":"Hoxha, B., Mavridis, N., Fainekos, G.E.: VISPEC: a graphical tool for elicitation of MTL requirements. In: Proceedings of IROS 2015: The 2015 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 3486\u20133492. IEEE (2015)","DOI":"10.1109\/IROS.2015.7353863"},{"key":"5_CR76","unstructured":"MathWorks, Inc.: Test generated code with SIL and PIL simulations, cf. https:\/\/www.mathworks.com\/help\/ecoder\/examples\/software-and-processor-in-the-loop-sil-and-pil-simulation.html"},{"key":"5_CR77","doi-asserted-by":"crossref","unstructured":"Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ni\u010dkovi\u0107, D.: From signal temporal logic to FPGA monitors. In: Proceedings of MEMOCODE 2015: The 13th ACM\/IEEE International Conference on Formal Methods and Models for Codesign, pp. 218\u2013227. IEEE (2015)","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"5_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-46982-9_13","volume-title":"Runtime Verification","author":"S Jak\u0161i\u0107","year":"2016","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Ni\u010dkovi\u0107, D.: Quantitative monitoring of STL with edit distance. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 201\u2013218. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_13"},{"key":"5_CR79","doi-asserted-by":"crossref","unstructured":"Jensen, J.C., Chang, D.H., Lee, E.A.: A model-based design methodology for cyber-physical systems. In: Proceedings of IEEE Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems (CyPhy), pp. 1666\u20131671. IEEE (2011)","DOI":"10.1109\/IWCMC.2011.5982785"},{"issue":"2","key":"5_CR80","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10009-013-0289-7","volume":"16","author":"Z Jiang","year":"2014","unstructured":"Jiang, Z., Pajic, M., Alur, R., Mangharam, R.: Closed-loop verification of medical devices with model abstraction and refinement. Int. J. Softw. Tools Technol. Transfer 16(2), 191\u2013213 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"5_CR81","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). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_14"},{"key":"5_CR82","doi-asserted-by":"crossref","unstructured":"Juniwal, G., Donz\u00e9, A., Jensen, J.C., Seshia, S.A.: CPSGrader: synthesizing temporal logic testers for auto-grading an embedded systems laboratory. In: Proceedings of EMSOFT 2014: The 2014 International Conference on Embedded Software, pp. 24:1\u201324:10. IEEE (2014)","DOI":"10.1145\/2656045.2656053"},{"key":"5_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-40787-1_9","volume-title":"Runtime Verification","author":"K Kalajdzic","year":"2013","unstructured":"Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S.D., Grosu, R.: Runtime verification with particle filtering. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 149\u2013166. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_9"},{"key":"5_CR84","unstructured":"Kane, A.: Runtime monitoring for safety-critical embedded systems. Ph.D. thesis, Carnegie Mellon University, College of Engineering (2015)"},{"key":"5_CR85","doi-asserted-by":"crossref","unstructured":"Kapinski, J., Jin, X., Deshmukh, J., Donz\u00e9, A., Yamaguchi, T., Ito, H., Kaga, T., Kobuna, S., Seshia, S.: ST-Lib: a library for specifying and classifying model behaviors. In: SAE Technical Paper. SAE International (2016)","DOI":"10.4271\/2016-01-0621"},{"key":"5_CR86","doi-asserted-by":"crossref","first-page":"1036","DOI":"10.2337\/dc15-0364","volume":"38","author":"A Kowalski","year":"2015","unstructured":"Kowalski, A.: Pathway to artificial pancreas revisited: moving downstream. Diabetes Care 38, 1036\u20131043 (2015)","journal-title":"Diabetes Care"},{"issue":"4","key":"5_CR87","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"5_CR88","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: Cyber physical systems: design challenges. In: Proceedings of ISORC 2011: The 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing, pp. 363\u2013369, May 2008","DOI":"10.1109\/ISORC.2008.25"},{"key":"5_CR89","unstructured":"Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Proceedings of PDPTA 1999: The International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 279\u2013287. CSREA Press (1999)"},{"issue":"4","key":"5_CR90","first-page":"328","volume":"13","author":"D Lemire","year":"2006","unstructured":"Lemire, D.: Streaming maximum-minimum filter using no more than three comparisons per element. Nord. J. Comput. 13(4), 328\u2013339 (2006)","journal-title":"Nord. J. Comput."},{"key":"5_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-11164-3_24","volume-title":"Runtime Verification","author":"Q Luo","year":"2014","unstructured":"Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: RV-Monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 285\u2013300. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_24"},{"issue":"7","key":"5_CR92","doi-asserted-by":"crossref","first-page":"1885","DOI":"10.2337\/dc13-2159","volume":"37","author":"DM Maahs","year":"2014","unstructured":"Maahs, D.M., Calhoun, P., Buckingham, B.A., et al.: A randomized trial of a home system to reduce nocturnal hypoglycemia in type 1 diabetes. Diabetes Care 37(7), 1885\u20131891 (2014)","journal-title":"Diabetes Care"},{"key":"5_CR93","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Prabhu, V.S.: Computing the Skorokhod distance between polygonal traces. In: Proceedings of HSCC 2015: The 18th International Conference on Hybrid Systems: Computation and Control, pp. 199\u2013208. ACM (2015)","DOI":"10.1145\/2728606.2728618"},{"key":"5_CR94","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Prabhu, V.S.: Computing distances between reach flowpipes. In: Proceedings of HSCC 2016: The 19th International Conference on Hybrid Systems: Computation and Control, pp. 267\u2013276. ACM (2016)","DOI":"10.1145\/2883817.2883850"},{"key":"5_CR95","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-46982-9_1","volume-title":"Runtime Verification","author":"O Maler","year":"2016","unstructured":"Maler, O.: Some thoughts on runtime verification. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 3\u201314. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_1"},{"key":"5_CR96","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT 2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"issue":"3","key":"5_CR97","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler, O., Ni\u010dkovi\u0107, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247\u2013268 (2013)","journal-title":"STTT"},{"key":"5_CR98","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-78127-1_26","volume-title":"Pillars of Computer Science","author":"O Maler","year":"2008","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 475\u2013505. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78127-1_26"},{"issue":"3","key":"5_CR99","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1177\/193229680700100303","volume":"1","author":"CD Man","year":"2007","unstructured":"Man, C.D., Raimondo, D.M., Rizza, R.A., Cobelli, C.: GIM, simulation software of meal glucose-insulin model. J. Diabetes Sci. Tech. 1(3), 323\u2013330 (2007)","journal-title":"J. Diabetes Sci. Tech."},{"key":"5_CR100","doi-asserted-by":"crossref","unstructured":"Mobilia, N., Donz\u00e9, A., Marc Moulis, J., Fanchon, E.: Producing a set of models for the iron homeostasis network. In: Proceedings of HSB 2013: The Second International Workshop on Hybrid Systems and Biology. EPTCS, vol. 125, pp. 92\u201398 (2013)","DOI":"10.4204\/EPTCS.125.7"},{"key":"5_CR101","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/7.4.308","volume":"7","author":"JA Nelder","year":"1965","unstructured":"Nelder, J.A., Mead, R.: A simplex method for function minimization. Comput. J. 7, 308\u2013313 (1965)","journal-title":"Comput. J."},{"key":"5_CR102","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-23820-3_2","volume-title":"Runtime Verification","author":"L Nenzi","year":"2015","unstructured":"Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 21\u201337. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_2"},{"key":"5_CR103","doi-asserted-by":"crossref","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivancic, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of HSCC 2010: The 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 211\u2013220. ACM (2010)","DOI":"10.1145\/1755952.1755983"},{"key":"5_CR104","doi-asserted-by":"crossref","unstructured":"Nguyen, L., Kapinski, J., Jin, X., Deshmukh, J., Butts, K., Johnson, T.: Abnormal data classification using time-frequency temporal logic. In: Proceedings of HSCC 2017: The 20th ACM International Conference on Hybrid Systems: Computation and Control, pp. 237\u2013242. ACM (2017)","DOI":"10.1145\/3049797.3049809"},{"key":"5_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-319-47169-3_28","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"T Nguyen","year":"2016","unstructured":"Nguyen, T., Bartocci, E., Ni\u010dkovi\u0107, D., Grosu, R., Jaksic, S., Selyunin, K.: The HARMONIA project: hardware monitoring for automotive systems-of-systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 371\u2013379. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47169-3_28"},{"key":"5_CR106","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-10702-8_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"T Nguyen","year":"2014","unstructured":"Nguyen, T., Ni\u010dkovi\u0107, D.: Assertion-based monitoring in practice \u2013 checking correctness of an automotive sensor interface. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 16\u201332. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10702-8_2"},{"key":"5_CR107","unstructured":"Nickovic, D.: Checking timed and hybrid properties: theory and applications. Ph.D. thesis. Universit\u00e9 Joseph Fourier, Grenoble, France (2008)"},{"key":"5_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-75454-1_22","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"D Nickovic","year":"2007","unstructured":"Nickovic, D., Maler, O.: AMT: a property-based monitoring tool for analog systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304\u2013319. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_22"},{"issue":"1","key":"5_CR109","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1109\/TII.2012.2226594","volume":"10","author":"M Pajic","year":"2014","unstructured":"Pajic, M., Mangharam, R., Sokolsky, O., Arney, D., Goldman, J., Lee, I.: Model-driven safety analysis of closed-loop medical systems. IEEE Trans. Ind. Inform. 10(1), 3\u201316 (2014)","journal-title":"IEEE Trans. Ind. Inform."},{"key":"5_CR110","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR111","doi-asserted-by":"crossref","unstructured":"Raman, V., Donz\u00e9, A., Sadigh, D., M. Murray, R., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: Proceedings of the HSCC 2015: The 18th International Conference on Hybrid Systems: Computation and Control, pp. 239\u2013248. ACM (2015)","DOI":"10.1145\/2728606.2728628"},{"key":"5_CR112","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-46982-9_3","volume-title":"Runtime Verification","author":"G Reger","year":"2016","unstructured":"Reger, G., Hall\u00e9, S., Falcone, Y.: Third international competition on runtime verification. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 21\u201337. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_3"},{"key":"5_CR113","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-88562-7_19","volume-title":"Computational Methods in Systems Biology","author":"A Rizk","year":"2008","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNAI), vol. 5307, pp. 251\u2013268. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88562-7_19"},{"key":"5_CR114","doi-asserted-by":"crossref","unstructured":"Rodionova, A., Bartocci, E., Ni\u010dkovi\u0107, D., Grosu, R.: Temporal logic as filtering. In: Proceedings of HSCC 2016: The 19th International Conference on Hybrid Systems: Computation and Control, pp. 11\u201320. ACM (2016)","DOI":"10.1145\/2883817.2883839"},{"key":"5_CR115","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of HSCC 2012: The 15th ACM International Conference on Hybrid Systems: Computation and Control, pp. 125\u2013134. ACM (2012)","DOI":"10.1145\/2185632.2185653"},{"issue":"2","key":"5_CR116","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1145\/3076125.3076128","volume":"14","author":"S Sankaranarayanan","year":"2017","unstructured":"Sankaranarayanan, S., Kumar, S.A., Cameron, F., Bequette, B.W., Fainekos, G.E., Maahs, D.M.: Model-based falsification of an artificial pancreas control system. SIGBED Rev. 14(2), 24\u201333 (2017)","journal-title":"SIGBED Rev."},{"key":"5_CR117","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Miller, C., Raghunathan, R., Ravanbakhsh, H., Fainekos, G.E.: A model-based approach to synthesizing insulin infusion pump usage parameters for diabetic patients. In: Proceedings of the 50th Annual Allerton Conference on Communication, Control, and Computing, pp. 1610\u20131617. IEEE (2012)","DOI":"10.1109\/Allerton.2012.6483413"},{"key":"5_CR118","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-319-63387-9_17","volume-title":"Computer Aided Verification","author":"K Selyunin","year":"2017","unstructured":"Selyunin, K., Jaksic, S., Nguyen, T., Reidl, C., Hafner, U., Bartocci, E., Nickovic, D., Grosu, R.: Runtime monitoring with recovery of the SENT communication protocol. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 336\u2013355. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_17"},{"key":"5_CR119","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-46982-9_30","volume-title":"Runtime Verification","author":"K Selyunin","year":"2016","unstructured":"Selyunin, K., Nguyen, T., Bartocci, E., Grosu, R.: Applying runtime monitoring for automotive electronic development. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 462\u2013469. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_30"},{"key":"5_CR120","doi-asserted-by":"crossref","unstructured":"Short, M., Pont, M.J.: Hardware in the loop simulation of embedded automotive control system. In: Proceedings of 2005 IEEE Intelligent Transportation Systems, pp. 426\u2013431. IEEE, September 2005","DOI":"10.1109\/ITSC.2005.1520052"},{"key":"5_CR121","doi-asserted-by":"crossref","first-page":"1621","DOI":"10.1177\/193229681300700623","volume":"7","author":"GM Steil","year":"2013","unstructured":"Steil, G.M.: Algorithms for a closed-loop artificial pancreas: the case for proportional-integral-derivative control. J. Diabetes Sci. Technol. 7, 1621\u20131631 (2013)","journal-title":"J. Diabetes Sci. Technol."},{"issue":"2","key":"5_CR122","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.addr.2003.08.011","volume":"56","author":"G Steil","year":"2004","unstructured":"Steil, G., Panteleon, A., Rebrin, K.: Closed-sloop insulin delivery - the path to physiological glucose control. Adv. Drug Deliv. Rev. 56(2), 125\u2013144 (2004)","journal-title":"Adv. Drug Deliv. Rev."},{"issue":"5","key":"5_CR123","doi-asserted-by":"crossref","first-page":"e1003056","DOI":"10.1371\/journal.pcbi.1003056","volume":"9","author":"S Stoma","year":"2013","unstructured":"Stoma, S., Donz\u00e9, A., Bertaux, F., Maler, O., Batt, G.: STL-based analysis of TRAIL-induced apoptosis challenges the notion of type I\/type II cell line classification. PLoS Comput. Biol. 9(5), e1003056 (2013)","journal-title":"PLoS Comput. Biol."},{"key":"5_CR124","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-319-10512-3_16","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"D Ulus","year":"2014","unstructured":"Ulus, D., Ferr\u00e8re, T., Asarin, E., Maler, O.: Timed pattern matching. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 222\u2013236. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10512-3_16"},{"key":"5_CR125","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"736","DOI":"10.1007\/978-3-662-49674-9_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Ulus","year":"2016","unstructured":"Ulus, D., Ferr\u00e8re, T., Asarin, E., Maler, O.: Online timed pattern matching using derivatives. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 736\u2013751. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_47"},{"key":"5_CR126","doi-asserted-by":"publisher","DOI":"10.1007\/b137011","volume-title":"A Practical Guide for SystemVerilog Assertions","author":"S Vijayaraghavan","year":"2006","unstructured":"Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, New York (2006). https:\/\/doi.org\/10.1007\/b137011"},{"issue":"5","key":"5_CR127","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1049\/iet-sen:20060076","volume":"1","author":"C Watterson","year":"2007","unstructured":"Watterson, C., Heffernan, D.: Runtime verification and monitoring of embedded systems. IET Softw. 1(5), 172\u2013179 (2007)","journal-title":"IET Softw."},{"key":"5_CR128","doi-asserted-by":"crossref","first-page":"934","DOI":"10.2337\/dc07-1967","volume":"31","author":"S Weinzimer","year":"2008","unstructured":"Weinzimer, S., Steil, G., Swan, K., Dziura, J., Kurtz, N., Tamborlane, W.: Fully automated closed-loop insulin delivery versus semiautomated hybrid control in pediatric patients with type 1 diabetes using an artificial pancreas. Diabetes Care 31, 934\u2013939 (2008)","journal-title":"Diabetes Care"},{"key":"5_CR129","doi-asserted-by":"crossref","unstructured":"Xiaoqing, J., Donz\u00e9, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: Proceedings of HSCC 2013: The ACM International Conference on Hybrid Systems: Computation and Control, pp. 43\u201352. ACM (2013)","DOI":"10.1145\/2461328.2461337"},{"key":"5_CR130","doi-asserted-by":"crossref","unstructured":"Yaghoubi, S., Fainekos, G.: Hybrid approximate gradient and stochastic descent for falsification of nonlinear systems. In: Proceedings of ACC 2017: The 2017 American Control Conference, pp. 529\u2013534. IEEE (2017)","DOI":"10.23919\/ACC.2017.7963007"},{"key":"5_CR131","doi-asserted-by":"crossref","unstructured":"Yamaguchi, T., Kaga, T., Donz\u00e9, A., Seshia, S.A.: Combining requirement mining, software model checking, and simulation-based verification for industrial automotive systems. In: Proceedings of FMCAD 2016: The 16th International Conference on Formal Methods in Computer-Aided Design, pp. 201\u2013204 (2016)","DOI":"10.1109\/FMCAD.2016.7886680"},{"key":"5_CR132","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-34691-0_11","volume-title":"Testing Software and Systems","author":"H Yang","year":"2012","unstructured":"Yang, H., Hoxha, B., Fainekos, G.: Querying parametric temporal logic properties on embedded systems. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol. 7641, pp. 136\u2013151. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34691-0_11"}],"container-title":["Lecture Notes in Computer Science","Lectures on Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-75632-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T17:44:21Z","timestamp":1751391861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-75632-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319756318","9783319756325"],"references-count":132,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}