{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:01:14Z","timestamp":1743138074197,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720124"},{"type":"electronic","value":"9783030720131"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present , an extensible Stream Runtime Verification (SRV) tool, that borrows from the functional language Haskell (1) rich types for data in events and verdicts; and (2) functional features for parametrization, libraries, high-order specification transformations, etc.<\/jats:p><jats:p>SRV is a formal dynamic analysis technique that generalizes Runtime Verification (RV) algorithms from temporal logics like LTL to stream monitoring, allowing the computation of verdicts richer than Booleans (quantitative values and beyond). The keystone of SRV is the clean separation between temporal dependencies and data computations. However, in spite of this theoretical separation previous engines include hardwired implementations of just a few datatypes, requiring complex changes in the tool chain to incorporate new data types. Additionally, when previous tools implement features like parametrization these are implemented in an ad-hoc way. In contrast, is implemented as a Haskell embedded DSL, borrowing datatypes and functional aspects from Haskell, resulting in an extensible engine (The tool is available open-source at<jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"http:\/\/github.com\/imdea-software\/hlola\">http:\/\/github.com\/imdea-software\/hlola<\/jats:ext-link>). We illustrate through several examples, including a UAV monitoring infrastructure with predictive characteristics that has been validated in online runtime verification in real mission planning.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_18","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"349-356","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["HLola: a Very Functional Tool for Extensible Stream Runtime Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3478-3408","authenticated-orcid":false,"given":"Felipe","family":"Gorostiaga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. Rule-based runtime verification. In Proc. of the 5th Int\u2019l Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI\u201904), volume 2937 of LNCS, pages 44\u201357. Springer, 2004.","key":"18_CR1","DOI":"10.1007\/978-3-540-24622-0_5"},{"unstructured":"Howard Barringer and Klaus Havelund. Tracecontract: A scala DSL for trace analysis. In Michael\u00a0J. Butler and Wolfram Schulte, editors, FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings, volume 6664 of Lecture Notes in Computer Science, pages 57\u201372. Springer, 2011.","key":"18_CR2"},{"doi-asserted-by":"crossref","unstructured":"Howard Barringer, David Rydeheard, and Klaus Havelund. Rule systems for run-time monitoring: From eagle to ruler. In Oleg Sokolsky and Serdar Ta\u015f\u0131ran, editors, Runtime Verification, pages 111\u2013125, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.","key":"18_CR3","DOI":"10.1007\/978-3-540-77395-5_10"},{"doi-asserted-by":"crossref","unstructured":"Ezio Bartocci and Yli\u00e8s Falcone, editors. Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of LNCS. Springer, 2018.","key":"18_CR4","DOI":"10.1007\/978-3-319-75632-5"},{"doi-asserted-by":"crossref","unstructured":"Andreas Bauer, Martin Leucker, and Chrisitan Schallhart. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology, 20(4):14, 2011.","key":"18_CR5","DOI":"10.1145\/2000799.2000800"},{"doi-asserted-by":"crossref","unstructured":"Marco Benedetti and Alessandro Cimatti. Bounded model checking for past LTL. In Proc. of TACAS\u201903, volume 2619 of LNCS, pages 18\u201333. Springer, 2003.","key":"18_CR6","DOI":"10.1007\/3-540-36577-X_3"},{"doi-asserted-by":"crossref","unstructured":"Mart\u00edn Ceresa, Felipe Gorostiaga, and C\u00e9sar S\u00e1nchez. Declarative stream runtime verification (hlola). In Bruno C. d.\u00a0S. Oliveira, editor, Programming Languages and Systems, pages 25\u201343, Cham, 2020. Springer International Publishing.","key":"18_CR7","DOI":"10.1007\/978-3-030-64437-6_2"},{"doi-asserted-by":"crossref","unstructured":"Lukas Convent, Sebastian Hungerecker, Martin Leucker, Torben Scheffel, Malte Schmitz, and Daniel Thoma. TeSSLa: Temporal stream-based specification language. In Proc. of SBMF\u201918, volume 11254 of LNCS. Springer, 2018.","key":"18_CR8","DOI":"10.1007\/978-3-030-03044-5_10"},{"unstructured":"Ben D\u2019Angelo, Sriram Sankaranarayanan, C\u00e9sar S\u00e1nchez, Will Robinson, Bernd Finkbeiner, Henny\u00a0B. Sipma, Sandeep Mehrotra, and Zohar Manna. LOLA: Runtime monitoring of synchronous systems. In Proc. of the 12th Int\u2019l Symp. of Temporal Representation and Reasoning (TIME\u201905), pages 166\u2013174. IEEE CS Press, 2005.","key":"18_CR9"},{"doi-asserted-by":"crossref","unstructured":"Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, and David\u00a0Van Campenhout. Reasoning with temporal logic on truncated paths. In Proc. of the 15th Int\u2019l Conf. on Computer Aided Verification (CAV\u201903), volume 2725 of LNCS, pages 27\u201339. Springer, 2003.","key":"18_CR10","DOI":"10.1007\/978-3-540-45069-6_3"},{"doi-asserted-by":"crossref","unstructured":"Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger, Leander Tentrup, and Torfah Hazem. StreamLAB: Stream-based monitoring of cyber-physical systems. In Proc. of the 31st Int\u2019l Conf. on Computer-Aided Verification (CAV\u201919), volume 11561 of LNCS, pages 421\u2013431. Springer, 2019.","key":"18_CR11","DOI":"10.1007\/978-3-030-25540-4_24"},{"doi-asserted-by":"crossref","unstructured":"Felipe Gorostiaga and C\u00e9sar S\u00e1nchez. Striver: Stream runtime verification for real-time event-streams. In Proc. of the 18th Int\u2019l Conf. on Runtime Verification (RV\u201918), volume 11237 of LNCS, pages 282\u2013298. Springer, 2018.","key":"18_CR12","DOI":"10.1007\/978-3-030-03769-7_16"},{"doi-asserted-by":"crossref","unstructured":"Klaus Havelund. Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Transf., 17(2):143\u2013170, 2015.","key":"18_CR13","DOI":"10.1007\/s10009-014-0309-2"},{"doi-asserted-by":"crossref","unstructured":"Klaus Havelund and Allen Goldberg. Verify your runs. In Proc. of VSTTE\u201905, LNCS 4171, pages 374\u2013383. Springer, 2005.","key":"18_CR14","DOI":"10.1007\/978-3-540-69149-5_40"},{"doi-asserted-by":"crossref","unstructured":"Klaus Havelund and Grigore Ro\u015fu. Synthesizing monitors for safety properties. In Proc. of the 8th Int\u2019l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902), volume 2280 of LNCS, pages 342\u2013356. Springer-Verlag, 2002.","key":"18_CR15","DOI":"10.1007\/3-540-46002-0_24"},{"doi-asserted-by":"crossref","unstructured":"Rudolph\u00a0Emil Kalman. A new approach to linear filtering and prediction problems. Transactions of the ASME\u2013Journal of Basic Engineering, 82(Series D):35\u201345, 1960.","key":"18_CR16","DOI":"10.1115\/1.3662552"},{"unstructured":"Martin Leucker, C\u00e9sar S\u00e1nchez, Torben Scheffel, Malte Schmitz, and Alexander Schramm. TeSSLa: Runtime verification of non-synchronized real-time streams. In Proc. of the 33rd Symposium on Applied Computing (SAC\u201918). ACM, 2018.","key":"18_CR17"},{"doi-asserted-by":"crossref","unstructured":"Martin Leucker and Christian Schallhart. A brief account of runtime verification. J. Logic Algebr. Progr., 78(5):293\u2013303, 2009.","key":"18_CR18","DOI":"10.1016\/j.jlap.2008.08.004"},{"doi-asserted-by":"crossref","unstructured":"Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems. Springer-Verlag, 1995.","key":"18_CR19","DOI":"10.1007\/978-1-4612-4222-2"},{"doi-asserted-by":"crossref","unstructured":"Jo\u00ebl Ouaknine and James Worrell. Some recent results in metric temporal logic. In Proc. of FORMATS\u201908, volume 5215 of LNCS, pages 1\u201313. Springer, 2008.","key":"18_CR20","DOI":"10.1007\/978-3-540-85778-5_1"},{"doi-asserted-by":"crossref","unstructured":"Grigore Ro\u015fu and Klaus Havelund. Rewriting-based techniques for runtime verification. Automated Software Engineering, 12(2):151\u2013197, 2005.","key":"18_CR21","DOI":"10.1007\/s10515-005-6205-y"},{"doi-asserted-by":"crossref","unstructured":"C\u00e9sar S\u00e1nchez. Online and offline stream runtime verification of synchronous systems. In Proc. of the 18th Int\u2019l Conf. on Runtime Verification (RV\u201918), volume 11237 of LNCS, pages 138\u2013163. Springer, 2018.","key":"18_CR22","DOI":"10.1007\/978-3-030-03769-7_9"},{"doi-asserted-by":"crossref","unstructured":"Koushik Sen and Grigore Ro\u015fu. Generating optimal monitors for extended regular expressions. In Oleg Sokolsky and Mahesh Viswanathan, editors, Electronic Notes in Theoretical Computer Science, volume\u00a089. Elsevier, 2003.","key":"18_CR23","DOI":"10.1016\/S1571-0661(04)81051-X"},{"doi-asserted-by":"crossref","unstructured":"Volker Stolz and Frank Huch. Runtime verification of concurrent haskell programs. Electron. Notes Theor. Comput. Sci., 113:201\u2013216, 2005.","key":"18_CR24","DOI":"10.1016\/j.entcs.2004.01.026"},{"doi-asserted-by":"crossref","unstructured":"Sebasti\u00e1n Zudaire, Felipe Gorostiaga, C\u00e9sar S\u00e1nchez, Gerardo Schneider, and Sebasti\u00e1n Uchitel. Assumption monitoring using runtime verification for UAV temporal task plan executions. Under submission, 2020.","key":"18_CR25","DOI":"10.1109\/ICRA48506.2021.9561671"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:44:39Z","timestamp":1671684279000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","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":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}