{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:55Z","timestamp":1749318115551,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031720437"},{"type":"electronic","value":"9783031720444"}],"license":[{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-72044-4_1","type":"book-chapter","created":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:02:41Z","timestamp":1725897761000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Temporal Logic Runtime Monitoring for\u00a0Tiny Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8315-1431","authenticated-orcid":false,"given":"R\u00fcdiger","family":"Ehlers","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,10]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-030-01090-4_20","volume-title":"Automated Technology for Verification and Analysis","author":"K Adabala","year":"2018","unstructured":"Adabala, K., Ehlers, R.: A fragment of linear temporal logic for universal very weak automata. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 335\u2013351. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_20"},{"issue":"3","key":"1_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification - Introductory and Advanced Topics. Lecture Notes in Computer Science, vol. 10457. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5","DOI":"10.1007\/978-3-319-75632-5"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-30446-1_4","volume-title":"Software Engineering and Formal Methods","author":"E Bartocci","year":"2019","unstructured":"Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Ni\u010dkovi\u0107, D.: Automatic failure explanation in CPS models. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 69\u201386. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_4"},{"issue":"3","key":"1_CR6","doi-asserted-by":"publisher","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. Log. Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Log. Comput."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011)","DOI":"10.1145\/2000799.2000800"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Baumeister, J., Finkbeiner, B., Schwenger, M., Torfah, H.: FPGA stream-monitoring of real-time properties. ACM Trans. Embed. Comput. Syst. 18(5s), 88:1\u201388:24 (2019)","DOI":"10.1145\/3358220"},{"issue":"1","key":"1_CR9","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/s10703-011-0132-2","volume":"40","author":"I Beer","year":"2012","unstructured":"Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.J.: Explaining counterexamples using causality. Formal Methods Syst. Des. 40(1), 20\u201340 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-21437-0_9","volume-title":"FM 2011: Formal Methods","author":"B Bonakdarpour","year":"2011","unstructured":"Bonakdarpour, B., Navabpour, S., Fischmeister, S.: Sampling-based runtime verification. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 88\u2013102. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_9"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-31980-1_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Chen","year":"2005","unstructured":"Chen, F., Ro\u015fu, G.: Java-MOP: a monitoring oriented programming environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546\u2013550. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_36"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11513988_36","volume-title":"Computer Aided Verification","author":"M d\u2019Amorim","year":"2005","unstructured":"d\u2019Amorim, M., Ro\u015fu, G.: Efficient monitoring of $$\\omega $$-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364\u2013378. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_36"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-031-13188-2_9","volume-title":"Computer Aided Verification","author":"A Duret-Lutz","year":"2022","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9"},{"key":"1_CR14","unstructured":"Efabless Corporation: Caravel system on chip (2021). https:\/\/github.com\/efabless\/caravel"},{"key":"1_CR15","unstructured":"Efabless Corporation: The open MPW program (2022). https:\/\/efabless.com\/open_shuttle_program"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-29860-8_34","volume-title":"Runtime Verification","author":"R Ehlers","year":"2012","unstructured":"Ehlers, R., Finkbeiner, B.: Monitoring realizability. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 427\u2013441. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_34"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Ehlers, R.: Runtime monitoring example data\/TAP 2024 (2024). https:\/\/doi.org\/10.5281\/zenodo.12789827","DOI":"10.5281\/zenodo.12789827"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-030-25540-4_24","volume-title":"Computer Aided Verification","author":"P Faymonville","year":"2019","unstructured":"Faymonville, P., et al.: StreamLAB: stream-based monitoring of cyber-physical systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 421\u2013431. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_24"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-24953-7_20","volume-title":"Automated Technology for Verification and Analysis","author":"T Ferr\u00e8re","year":"2015","unstructured":"Ferr\u00e8re, T., Maler, O., Ni\u010dkovi\u0107, D.: Trace diagnostics using temporal implicants. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 241\u2013258. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_20"},{"issue":"2","key":"1_CR20","doi-asserted-by":"publisher","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. Notes Theor. Comput. Sci. 55(2), 200\u2013217 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"issue":"3","key":"1_CR22","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp. 531\u2013542. IEEE (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"1_CR24","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-031-28916-3_3","volume-title":"Advanced Boolean Techniques","author":"SY Lee","year":"2023","unstructured":"Lee, S.Y., Riener, H., De Micheli, G.: External don\u2019t cares in logic synthesis. In: Drechsler, R., Huhn, S. (eds.) Advanced Boolean Techniques, pp. 33\u201347. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-28916-3_3"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: 41st Annual Symposium on Foundations of Computer Science (FOCS), pp. 643\u2013652 (2000)","DOI":"10.1109\/SFCS.2000.892332"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Medhat, R., Kumar, D., Bonakdarpour, B., Fischmeister, S.: Sacrificing a little space can significantly improve monitoring of time-sensitive cyber-physical systems. In: ACM\/IEEE International Conference on Cyber-Physical Systems (ICCPS), pp. 115\u2013126 (2014)","DOI":"10.1109\/ICCPS.2014.6843716"},{"issue":"1","key":"1_CR27","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10703-017-0275-x","volume":"51","author":"P Moosbrugger","year":"2017","unstructured":"Moosbrugger, P., Rozier, K.Y., Schumann, J.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. Formal Methods Syst. Des. 51(1), 31\u201361 (2017)","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"1_CR28","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s11334-013-0223-x","volume":"9","author":"L Pike","year":"2013","unstructured":"Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: monitoring embedded systems. Innov. Syst. Softw. Eng. 9(4), 235\u2013255 (2013)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-24431-5_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"T Reinbacher","year":"2011","unstructured":"Reinbacher, T., Brauer, J., Horauer, M., Steininger, A., Kowalewski, S.: Past time LTL runtime verification for microcontroller binary code. In: Sala\u00fcn, G., Sch\u00e4tz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 37\u201351. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24431-5_5"},{"key":"1_CR31","unstructured":"Reinbacher, T., Horauer, M., Steininger, A.: A runtime verification unit for microcontrollers. In: Proceedings of the 2012 System, Software, SoC and Silicon Debug Conference, pp.\u00a01\u20136 (2012)"},{"key":"1_CR32","unstructured":"Snook, C.F.: Exploring the barriers to formal specification. Ph.D. thesis, University of Southampton, UK (2001). https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.268626"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Solet, D., B\u00e9chennec, J., Briday, M., Faucou, S., Pillement, S.: Hardware runtime verification of embedded software in SoPC. In: 11th IEEE Symposium on Industrial Embedded Systems (SIES), pp. 171\u2013176. IEEE (2016)","DOI":"10.1109\/SIES.2016.7509425"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248\u2013263. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_21"},{"issue":"3","key":"1_CR35","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. Formal Methods Syst. Des. 41(3), 236\u2013268 (2012)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"1_CR36","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/2967606","volume":"60","author":"FW Vaandrager","year":"2017","unstructured":"Vaandrager, F.W.: Model learning. Commun. ACM 60(2), 86\u201395 (2017)","journal-title":"Commun. ACM"},{"issue":"1","key":"1_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Walters, G., King, E., Kessinger, R., Fryer, R.: Processor design and implementation for real-time testing of embedded systems. In: 17th DASC. AIAA\/IEEE\/SAE Digital Avionics Systems Conference, vol.\u00a01, pp. B44\u20131. IEEE (1998)","DOI":"10.1109\/DASC.1998.741470"},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-319-23820-3_16","volume-title":"Runtime Verification","author":"S Wang","year":"2015","unstructured":"Wang, S., Geoffroy, Y., G\u00f6ssler, G., Sokolsky, O., Lee, I.: A hybrid approach to causality analysis. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 250\u2013265. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_16"},{"key":"1_CR40","unstructured":"Wolf, C.X.: Reference hardware implementations of bit extract\/deposit instructions (2017). https:\/\/github.com\/cliffordwolf\/bextdep"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-72044-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:05:19Z","timestamp":1725897919000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-72044-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,10]]},"ISBN":["9783031720437","9783031720444"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-72044-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,10]]},"assertion":[{"value":"10 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}