{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:28:06Z","timestamp":1777519686210,"version":"3.51.4"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633862","type":"print"},{"value":"9783319633879","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63387-9_17","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"336-355","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Runtime Monitoring with Recovery of the SENT Communication Protocol"],"prefix":"10.1007","author":[{"given":"Konstantin","family":"Selyunin","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Jaksic","sequence":"additional","affiliation":[]},{"given":"Thang","family":"Nguyen","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Reidl","sequence":"additional","affiliation":[]},{"given":"Udo","family":"Hafner","sequence":"additional","affiliation":[]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"given":"Dejan","family":"Nickovic","sequence":"additional","affiliation":[]},{"given":"Radu","family":"Grosu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"17_CR1","unstructured":"ISO 26262: \u201cRoad vehicles \u2013 Functional safety\u201d. International Organization for Standardization (ISO) (2011)"},{"key":"17_CR2","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Broy, M., Krcmar, H., Kirstan, S., Sch\u00e4tz, B.: What is the benefit of a model-based design of embedded software systems in the car industry? In: Emerging Technologies for the Evolution and Maintenance of Software Models, pp. 310\u2013337 (2012)","DOI":"10.4018\/978-1-4666-4301-7.ch017"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-29860-8_4","volume-title":"Runtime Verification","author":"M Leucker","year":"2012","unstructured":"Leucker, M.: Teaching runtime verification. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 34\u201348. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-29860-8_4"},{"key":"17_CR5","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 (2017)","DOI":"10.1007\/s10009-017-0454-5"},{"key":"17_CR6","unstructured":"SAE International. SENT - Single Edge Nibble Transmission for Automotive Applications, J2716, Standard (2016). http:\/\/standards.sae.org\/j2716_201001\/. Accessed 21 Jan 2017"},{"key":"17_CR7","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). doi:10.1007\/978-3-540-75454-1_22"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-77395-5_1","volume-title":"Runtime Verification","author":"C Eisner","year":"2007","unstructured":"Eisner, C.: PSL for runtime verification: theory and practice. In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 1\u20138. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-77395-5_1"},{"key":"17_CR9","volume-title":"A Practical Guide for SystemVerilog Assertions","author":"S Vijayaraghavan","year":"2014","unstructured":"Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer Publishing Company Incorporated, Heidelberg (2014)"},{"key":"17_CR10","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). doi:10.1007\/978-3-642-33386-6_9"},{"issue":"3","key":"17_CR11","doi-asserted-by":"publisher","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. Int. J. Softw. Tools Technol. Transf. 15(3), 247\u2013268 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"17_CR12","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 Part II. LNCS, vol. 9207, pp. 322\u2013337. Springer, Cham (2015). doi:10.1007\/978-3-319-21668-3_19"},{"key":"17_CR13","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"},{"key":"17_CR14","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":"3","key":"17_CR15","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for systemc. Form. Methods Syst. Des. 41(3), 236\u2013268 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-319-23820-3_15","volume-title":"Runtime Verification","author":"J Schumann","year":"2015","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 233\u2013249. Springer, Cham (2015). doi:10.1007\/978-3-319-23820-3_15"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Boule, M., Zilic, Z.: Efficient automata-based assertion-checker synthesis of PSL properties. In: 2006 IEEE International High Level Design Validation and Test Workshop, pp. 69\u201376 (2006)","DOI":"10.1109\/HLDVT.2006.319966"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-69850-0_11","volume-title":"25 Years of Model Checking","author":"A Pnueli","year":"2008","unstructured":"Pnueli, A., Zaks, A.: On the merits of temporal testers. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 172\u2013195. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-69850-0_11"},{"issue":"2","key":"17_CR19","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/s10703-009-0085-x","volume":"36","author":"KD Jones","year":"2010","unstructured":"Jones, K.D., Konrad, V., Nickovic, D.: Analog property checkers: a DDR2 case study. Form. Methods Syst. Des. 36(2), 114\u2013130 (2010)","journal-title":"Form. Methods Syst. Des."},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1016\/j.scico.2015.11.002","volume":"118","author":"T Nguyen","year":"2016","unstructured":"Nguyen, T., Nickovic, D.: Assertion-based monitoring in practice - checking correctness of an automotive sensor interface. Sci. Comput. Program. 118, 40\u201359 (2016)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"17_CR21","doi-asserted-by":"publisher","first-page":"e1004591","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), e1004591 (2016)","journal-title":"PLoS Comput. Biol."},{"key":"17_CR22","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). doi:10.1007\/978-3-642-40708-6_13"},{"key":"17_CR23","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). doi:10.1007\/978-3-662-45231-8_30"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann. J.: Temporallogic based runtime observer pairs for system health management of real-time systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference (TACAS), Grenoble, France, pp. 357\u2013372 (2014)","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Dahan, A., Geist, D., Gluhovsky, L., Pidan, D., Shapir, G., Wolfsthal, Y., Benalycherif, L., Kamdem, R., Lahbib, Y.: Combining system level modeling with assertion based verification. In: 6th International Symposium on Quality of Electronic Design (ISQED) 21\u201323 March 2005, San Jose, CA, USA, pp. 310\u2013315 (2005)","DOI":"10.1109\/ISQED.2005.32"},{"key":"17_CR26","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). doi:10.1007\/978-3-540-78127-1_26"},{"issue":"2","key":"17_CR27","doi-asserted-by":"publisher","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":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-35632-2_13","volume-title":"Runtime Verification","author":"T Reinbacher","year":"2013","unstructured":"Reinbacher, T., F\u00fcgger, M., Brauer, J.: Real-time runtime verification on chip. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 110\u2013125. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-35632-2_13"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL\u2014a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). doi:10.1007\/BFb0020949"},{"issue":"1\u20132","key":"17_CR30","first-page":"134","volume":"1","author":"P Pettersson","year":"1997","unstructured":"Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1\u20132), 134\u2013152 (1997)","journal-title":"STTT"},{"key":"17_CR31","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). doi:10.1007\/978-3-319-10702-8_2"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: American Control Conference, ACC 2012, Montreal, QC, Canada, pp. 3567\u20133572 (2012)","DOI":"10.1109\/ACC.2012.6315384"},{"key":"17_CR33","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). doi:10.1007\/978-3-319-46982-9_30"},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/11867340_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"O Maler","year":"2006","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274\u2013289. Springer, Heidelberg (2006). doi:10.1007\/11867340_20"},{"key":"17_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73368-3_12","volume-title":"Computer Aided Verification","author":"O Maler","year":"2007","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: On synthesizing controllers from bounded-response properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 95\u2013107. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-73368-3_12"},{"key":"17_CR36","doi-asserted-by":"crossref","unstructured":"Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Nickovic, D.: From signal temporal logic to FPGA monitors. In: Proceedings of 13th ACM\/IEEE International Conference on Formal Methods and Models for Codesign, pp. 218\u2013227 (2015)","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"17_CR37","volume-title":"Serial Port Complete: COM Ports, USB Virtual COM Ports, and Ports for Embedded Systems","author":"J Axelson","year":"2007","unstructured":"Axelson, J.: Serial Port Complete: COM Ports, USB Virtual COM Ports, and Ports for Embedded Systems, 2nd edn. Lakeview Research, Madison (2007)","edition":"2"},{"key":"17_CR38","unstructured":"ANSI E1.11-2008 (R2013). Entertainment Technology \u2013 USITT DMX512-A \u2013 Asynchronous Serial Digital Data Transmission Standard for Controlling Lighting Equipment and Accessories (2008). http:\/\/webstore.ansi.org\/RecordDetail.aspx?sku=ANSI+E1.11-2008+(R2013). Accessed 20 Jan 2017"},{"key":"17_CR39","unstructured":"Xilinx Inc. Vivado Design Suite Tutorial, Programming and Debugging (2016). http:\/\/www.xilinx.com\/support\/documentation\/sw_manuals\/xilinx2016_2\/ug936-vivado-tutorial-programming-debugging.pdf. Accessed 12 Jan 2017"},{"key":"17_CR40","unstructured":"Xilinx Inc. Vivado High-Level Synthesis. http:\/\/www.xilinx.com\/products\/design-tools\/vivado\/integration\/esl-design.html. Accessed 18 Jan 2017"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:09:24Z","timestamp":1750554564000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}