{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:16:05Z","timestamp":1783545365875,"version":"3.55.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Stream-based monitoring is a runtime verification approach\u00a0where a\n                    <jats:italic>monitor<\/jats:italic>\n                    aggregates streams of input data from sensors and other sources to give real-time statistics and assessments of a system\u2019s health. One of the central challenges in designing reliable stream-based monitors is to deal with the asynchronous nature of data streams: in concrete applications, the different sensors being monitored produce values at different speeds, and it is the monitor\u2019s responsibility to correctly react to the asynchronous arrival of different streams of values. To ease this process, modern frameworks for stream-based monitoring such as\n                    <jats:sc>RTLola<\/jats:sc>\n                    enable users to finely specify data synchronization policies via a system of\n                    <jats:italic>pacing annotations<\/jats:italic>\n                    . While this feature simplifies the design of monitors, it can also lead users to write\n                    <jats:italic>inconsistent<\/jats:italic>\n                    policies, where synchronization between two streams is explicitly requested via annotations, but cannot always be achieved. To mitigate this issue, this paper presents\n                    <jats:italic>pacing types<\/jats:italic>\n                    , a novel type system implemented in RTLola to ensure that monitors for asynchronous streams are free of timing inconsistencies. We give a formal semantics to pacing annotations for a core fragment of\n                    <jats:sc>RTLola<\/jats:sc>\n                    , and present a soundness proof of the pacing type system. For an additional level of guarantees, we machine-checked the soundness proof using the Rocq proof assistant.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_8","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:20:35Z","timestamp":1779024035000},"page":"154-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Pacing Types for\u00a0Asynchronous Stream Equations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9672-2398","authenticated-orcid":false,"given":"Florian","family":"Kohn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2307-2296","authenticated-orcid":false,"given":"Arthur","family":"Correnson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8891-7483","authenticated-orcid":false,"given":"Jan","family":"Baumeister","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-319-63387-9_18","volume-title":"Computer Aided Verification","author":"D Basin","year":"2017","unstructured":"Basin, D., Klaedtke, F., Z\u0103linescu, E.: Runtime verification of temporal properties over out-of-order data streams. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 356\u2013376. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_18"},{"issue":"4","key":"8_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. (TOSEM) 20(4), 1\u201364 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Baumeister, J., et al.: Monitoring unmanned aircraft: specification, integration, and lessons-learned. In: Gurfinkel, A., Ganesh, V., (eds.), Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, 24-27 July 2024, Proceedings, Part II, volume 14682 of Lecture Notes in Computer Science, pp. 207\u2013218. Springer (2024)","DOI":"10.1007\/978-3-031-65630-9_10"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Baumeister, J., Finkbeiner, B., Kohn, F., Scheerer, F.: A tutorial on stream-based monitoring. In: Platzer, A., Yvonne Rozier, K., Pradella, M., Rossi, M., (eds.), Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, 9-13 September 2024, Proceedings, Part II, vol. 14934 of Lecture Notes in Computer Science, pp. 624\u2013648. Springer (2024)","DOI":"10.1007\/978-3-031-71177-0_33"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Baumeister, J., Finkbeiner, B., Schirmer, S., Schwenger, M., Torens, C.: RTLola cleared for take-off: monitoring autonomous aircraft. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 28\u201339. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_3","DOI":"10.1007\/978-3-030-53291-8_3"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Bourke, T., Caillaud, B., Pagano, B., Pouzet, M.: A type-based analysis of causality loops in hybrid systems modelers. In: Fr\u00e4nzle, M., Lygeros, J., (eds.), 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC\u201914, Berlin, Germany, 15-17 April 2014, pp. 71\u201382. ACM (2014)","DOI":"10.1145\/2562059.2562125"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S., (eds.), Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, 9-14 October 2011, pp. 137\u2013148. ACM (2011)","DOI":"10.1145\/2038642.2038664"},{"key":"8_CR8","unstructured":"Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: Stephen\u00a0D. Brookes, A.\u00a0W. Roscoe, and Glynn Winskel, editors, Seminar on Concurrency, Carnegie-Mellon University, Pittsburg, PA, USA, 9-11 July 1984, volume 197 of Lecture Notes in Computer Science, pp. 389\u2013448. Springer (1984)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Chen, J., et al.: Synchronous programming with refinement types. Proc. ACM Program. Lang., 8(ICFP), 938\u2013972 (2024)","DOI":"10.1145\/3674657"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Cola\u00e7o, J.-L., Pouzet, M.: Clocks as first class abstract types. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 134\u2013155. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45212-6_10","DOI":"10.1007\/978-3-540-45212-6_10"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"d\u2019Angelo, B., et al.: Lola: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME\u201905), pp. 166\u2013174. IEEE (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-46982-9_10","volume-title":"Runtime Verification","author":"P Faymonville","year":"2016","unstructured":"Faymonville, P., Finkbeiner, B., Schirmer, S., Torfah, H.: A stream-based specification language for network monitoring. In: Falcone, Y., S\u00e1nchez, C. (eds.) Runtime Verification, pp. 152\u2013168. Springer International Publishing, Cham (2016)"},{"key":"8_CR13","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-030-25540-4_24"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Gautier, T., Le Guernic, P.: SIGNAL: a declarative language for synchronous programming of real-time systems. In: Kahn, G., (eds.), Functional Programming Languages and Computer Architecture, Portland, Oregon, USA, 14-16 September 1987, Proceedings, volume 274 of Lecture Notes in Computer Science, pp. 257\u2013277. Springer (1987)","DOI":"10.1007\/3-540-18317-5_15"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: HStriver: a very functional extensible tool for the runtime verification of real-time event streams. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 563\u2013580. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_30","DOI":"10.1007\/978-3-030-90870-6_30"},{"issue":"9","key":"8_CR16","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Karimi, M., Kueffner, K., Mallik, K.: Monitoring algorithmic fairness. In: Enea, C., Lal, A., (eds.), Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17-22 July 2023, Proceedings, Part II, volume 13965 of Lecture Notes in Computer Science, pp. 358\u2013382. Springer (2023)","DOI":"10.1007\/978-3-031-37703-7_17"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Jin, D., O\u2019Neil Meredith, P., Lee, C., Rosu, G.: Javamop: efficient parametric runtime monitoring framework. In: Glinz, M., Murphy, G.C., Pezz\u00e8, M., (eds.), 34th International Conference on Software Engineering, ICSE 2012, 2-9 June 2012, Zurich, Switzerland, pp. 1427\u20131430. IEEE Computer Society (2012)","DOI":"10.1109\/ICSE.2012.6227231"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Junges, S., Torfah, H., Seshia, S.A.: Runtime monitors for markov decision processes. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 553\u2013576. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_26","DOI":"10.1007\/978-3-030-81688-9_26"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Kallwies, H., Leucker, M., Schmitz, M., Schulz, A., Thoma, D., Weiss, A.: Tessla - an ecosystem for runtime verification. In: Dang, T., Stolz, V., (eds.), Runtime Verification - 22nd International Conference, RV 2022, Tbilisi, Georgia, 28-30 September 2022, Proceedings, volume 13498 of Lecture Notes in Computer Science, pp. 314\u2013324. Springer (2022)","DOI":"10.1007\/978-3-031-17196-3_20"},{"key":"8_CR21","unstructured":"Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., Sokolsky, O.: Formally specified monitoring of temporal properties. In: 11th Euromicro Conference on Real-Time Systems (ECRTS 1999), 9-11 June 1999, York, England, UK, Proceedings, pp. 114\u2013122. IEEE Computer Society (1999)"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Mandel, L., Plateau, F., Pouzet, M.: Lucy-n: a n-synchronous extension of Lustre. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 288\u2013309. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13321-3_17","DOI":"10.1007\/978-3-642-13321-3_17"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Perez, I., Goodloe, A.E., Dedden, F.: Runtime verification in real-time with the copilot language: a tutorial. In: Platzer, A., Yvonne Rozier, K., Pradella, M., Rossi, M., (eds.), Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, 9-13 September 2024, Proceedings, Part II, volume 14934 of Lecture Notes in Computer Science, pp. 469\u2013491. Springer (2024)","DOI":"10.1007\/978-3-031-71177-0_27"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:53Z","timestamp":1783542593000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}