{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T03:01:15Z","timestamp":1791342075318,"version":"4.3.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711763","type":"print"},{"value":"9783031711770","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Stream-based runtime monitoring frameworks are safety assurance tools that check the runtime behavior of a system against a formal specification. This tutorial provides a hands-on introduction to RTLola, a real-time monitoring toolkit for cyber-physical systems and networks. RTLola processes, evaluates, and aggregates streams of input data, such as sensor readings, and provides a real-time analysis in the form of comprehensive statistics and logical assessments of the system\u2019s health. RTLola has been applied successfully in monitoring autonomous systems such as unmanned aircraft. The tutorial guides the reader through the development of a stream-based specification for an autonomous drone observing other flying objects in its flight path. Each tutorial section provides an intuitive introduction, highlighting useful language features and specification patterns, and gives a more in-depth explanation of technical details for the advanced reader. Finally, we discuss how runtime monitors generated from RTLola specifications can be integrated into a variety of systems and discuss different monitoring applications.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_33","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"624-648","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Tutorial on\u00a0Stream-Based Monitoring"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8891-7483","authenticated-orcid":false,"given":"Jan","family":"Baumeister","sequence":"first","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9672-2398","authenticated-orcid":false,"given":"Florian","family":"Kohn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8115-0359","authenticated-orcid":false,"given":"Frederik","family":"Scheerer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"33_CR1","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":"33_CR2","unstructured":"Baumeister, J., et al.: Monitoring unmanned aircraft: specification, integration, and lessons-learned. In: Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, Canada, 22\u201327 July 2024. Accepted for publication (2024)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-030-60508-7_25","volume-title":"Runtime Verification","author":"J Baumeister","year":"2020","unstructured":"Baumeister, J., Finkbeiner, B., Kruse, M., Schwenger, M.: Automatic optimizations for stream-based monitoring languages. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 451\u2013461. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_25"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-030-53291-8_3","volume-title":"Computer Aided Verification","author":"J Baumeister","year":"2020","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"},{"key":"33_CR5","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3358220","DOI":"10.1145\/3358220"},{"issue":"2","key":"33_CR6","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/S10009-022-00689-5","volume":"25","author":"S Biewer","year":"2023","unstructured":"Biewer, S., Finkbeiner, B., Hermanns, H., K\u00f6hl, M.A., Schnitzer, Y., Schwenger, M.: On the road with RTLola. Int. J. Softw. Tools Technol. Transf. 25(2), 205\u2013218 (2023). https:\/\/doi.org\/10.1007\/S10009-022-00689-5","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-030-03044-5_10","volume-title":"Formal Methods: Foundations and Applications","author":"L Convent","year":"2018","unstructured":"Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: temporal stream-based specification language. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 144\u2013162. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03044-5_10"},{"key":"33_CR8","doi-asserted-by":"publisher","unstructured":"D\u2019Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23\u201325 June 2005, Burlington, Vermont, USA, pp. 166\u2013174. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/TIME.2005.26","DOI":"10.1109\/TIME.2005.26"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-030-88494-9_4","volume-title":"Runtime Verification","author":"JC Dauer","year":"2021","unstructured":"Dauer, J.C., Finkbeiner, B., Schirmer, S.: Monitoring with verified guarantees. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 62\u201380. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_4"},{"key":"33_CR10","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D.A., Kalus, G. (eds.) Engineering Dependable Software Systems, NATO Science for Peace and Security Series, D: Information and Communication Security, vol.\u00a034, pp. 141\u2013175. IOS Press (2013). https:\/\/doi.org\/10.3233\/978-1-61499-207-3-141","DOI":"10.3233\/978-1-61499-207-3-141"},{"issue":"2","key":"33_CR11","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/S10009-021-00609-Z","volume":"23","author":"Y Falcone","year":"2021","unstructured":"Falcone, Y., Krstic, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. 23(2), 255\u2013284 (2021). https:\/\/doi.org\/10.1007\/S10009-021-00609-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","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.) RV 2016. LNCS, vol. 10012, pp. 152\u2013168. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_10"},{"key":"33_CR13","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":"33_CR14","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Keller, A., Schmidt, J., Schwenger, M.: Robust monitoring for medical cyber-physical systems. In: Proceedings of the Workshop on Medical Cyber Physical Systems and Internet of Medical Things, MCPS 2021, pp. 17\u201322. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3446913.3460318","DOI":"10.1145\/3446913.3460318"},{"key":"33_CR15","unstructured":"Finkbeiner, B., Kohn, F., Scheerer, F., Schledjewski, M.: The RTLola Playground (2023). https:\/\/rtlola.org\/playground"},{"key":"33_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-031-45332-8_13","volume-title":"ATVA 2023","author":"B Finkbeiner","year":"2023","unstructured":"Finkbeiner, B., Kohn, F., Schledjewski, M.: Leveraging static analysis: an IDE for RTLola. In: Andr\u00e9, \u00c9., Sun, J. (eds.) ATVA 2023. LNCS, vol. 14216, pp. 251\u2013262. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_13"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-030-60508-7_24","volume-title":"Runtime Verification","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Oswald, S., Passing, N., Schwenger, M.: Verified rust monitors for lola specifications. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 431\u2013450. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_24"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-030-03769-7_16","volume-title":"Runtime Verification","author":"F Gorostiaga","year":"2018","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: Striver: stream runtime verification for real-time event-streams. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 282\u2013298. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_16"},{"issue":"5","key":"33_CR19","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/J.JLAP.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Methods Program. 78(5), 293\u2013303 (2009). https:\/\/doi.org\/10.1016\/J.JLAP.2008.08.004","journal-title":"J. Log. Algebraic Methods Program."},{"key":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-030-60508-7_5","volume-title":"Runtime Verification","author":"M Schwenger","year":"2020","unstructured":"Schwenger, M.: Monitoring cyber-physical systems: from design to integration. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 87\u2013106. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_5"},{"key":"33_CR21","doi-asserted-by":"publisher","unstructured":"Schwenger, M.: Statically-analyzed stream monitoring for cyber-physical systems (2022). https:\/\/doi.org\/10.22028\/D291-37014","DOI":"10.22028\/D291-37014"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-030-32079-9_6","volume-title":"Runtime Verification","author":"H Torfah","year":"2019","unstructured":"Torfah, H.: Stream-based monitors for real-time properties. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 91\u2013110. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_6"}],"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-031-71177-0_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:15:40Z","timestamp":1726121740000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","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":"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":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}