{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:23Z","timestamp":1740122723008,"version":"3.37.3"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100012818","name":"Comunidad de Madrid","doi-asserted-by":"publisher","award":["S2018\/TCS-4339 (BLOQUES-CM)"],"award-info":[{"award-number":["S2018\/TCS-4339 (BLOQUES-CM)"]}],"id":[{"id":"10.13039\/100012818","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004837","name":"Ministerio de Ciencia e Innovaci\u00f3n","doi-asserted-by":"publisher","award":["FPU18\/04362"],"award-info":[{"award-number":["FPU18\/04362"]}],"id":[{"id":"10.13039\/501100004837","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,8]]},"DOI":"10.1007\/s10703-023-00428-9","type":"journal-article","created":{"date-parts":[[2023,6,21]],"date-time":"2023-06-21T08:02:55Z","timestamp":1687334575000},"page":"3-34","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Runtime verification of real-time event streams using the tool HStriver"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3478-3408","authenticated-orcid":false,"given":"Felipe","family":"Gorostiaga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,6,21]]},"reference":[{"key":"428_CR1","doi-asserted-by":"crossref","unstructured":"Havelund K, Goldberg A (2005) Verify your runs. In: Proceedings of verified software: theories, tools, and experiments (VSTTE\u201905), LNCS, vol 4171. Springer, Heidelberg, pp 374\u2013383","DOI":"10.1007\/978-3-540-69149-5_40"},{"issue":"5","key":"428_CR2","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 (2009) A brief account of runtime verification. J Log Algebr Program 78(5):293\u2013303","journal-title":"J Log Algebr Program"},{"key":"428_CR3","doi-asserted-by":"crossref","unstructured":"Bartocci E, Falcone Y (eds) (2018) Lectures on runtime verification\u2014introductory and advanced topics. LNCS, vol 10457. Springer, Cham","DOI":"10.1007\/978-3-319-75632-5"},{"key":"428_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems. Springer, New York"},{"issue":"4","key":"428_CR5","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):14","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"428_CR6","doi-asserted-by":"crossref","unstructured":"Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: Proceedings of the 15th international conference on computer aided verification (CAV\u201903). LNCS, vol 2725. Springer, Heidelberg, pp 27\u201339","DOI":"10.1007\/978-3-540-45069-6_3"},{"key":"428_CR7","doi-asserted-by":"crossref","unstructured":"Havelund K, Ro\u015fu G (2002) Synthesizing monitors for safety properties. In: Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201902). LNCS, vol 2280. Springer, Heidelberg, pp 342\u2013356","DOI":"10.1007\/3-540-46002-0_24"},{"key":"428_CR8","doi-asserted-by":"crossref","unstructured":"Sen K, Ro\u015fu G (2003) Generating optimal monitors for extended regular expressions. In: Electronic notes in theoretical computer science, vol 89. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(04)81051-X"},{"issue":"2","key":"428_CR9","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G Ro\u015fu","year":"2005","unstructured":"Ro\u015fu G, Havelund K (2005) Rewriting-based techniques for runtime verification. Automat Softw Eng 12(2):151\u2013197","journal-title":"Automat Softw Eng"},{"key":"428_CR10","doi-asserted-by":"crossref","unstructured":"Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: Proceedings of the 5th international conference on verification, model checking and abstract interpretation (VMCAI\u201904). LNCS, vol 2937. Springer, Heidelberg, pp 44\u201357","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"428_CR11","doi-asserted-by":"crossref","unstructured":"Barringer H, Rydeheard D, Havelund K (2007) Rule systems for run-time monitoring: from Eagle to RuleR. In: Proceedings of the 7th international workshop on runtime verification (RV\u201907). LNCS, vol 4839. Springer, Heidelberg, pp 111\u2013125","DOI":"10.1007\/978-3-540-77395-5_10"},{"key":"428_CR12","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo B, Sankaranarayanan S, S\u00e1nchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: runtime monitoring of synchronous systems. In: Proceedings of the 12th international symposium of temporal representation and reasoning (TIME\u201905). IEEE CS Press, Washington DC, pp 166\u2013174","DOI":"10.1109\/TIME.2005.26"},{"key":"428_CR13","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez C (2018) Online and offline stream runtime verification of synchronous systems. In: Proceedings of the 18th international conference on runtime verification (RV\u201918). LNCS, vol 11237. Springer, Cham, pp 138\u2013163","DOI":"10.1007\/978-3-030-03769-7_9"},{"key":"428_CR14","doi-asserted-by":"crossref","unstructured":"Berry G (2000) The foundations of Esterel. Proof, language, and interaction: essays in honour of Robin Milner. MIT Press, Cambridge, MA, pp 425\u2013454","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"428_CR15","unstructured":"Halbwachs N, Caspi P, Pilaud D, Plaice JA (1987) Lustre: a declarative language for programming synchronous systems. In: Proceedings of the 14th ACM symposium on principles of programming languages (POPL\u201987). ACM Press, New York, NY, pp 178\u2013188"},{"key":"428_CR16","doi-asserted-by":"crossref","unstructured":"Convent L, Hungerecker S, Leucker M, Scheffel T, Schmitz M, Thoma D (2018) TeSSLa: temporal stream-based specification language. In: Proceedings of the 21st. Brazilian symposium on formal methods (SBMF\u201918). LNCS, vol 11254. Springer, Cham","DOI":"10.1007\/978-3-030-03044-5_10"},{"key":"428_CR17","doi-asserted-by":"crossref","unstructured":"Leucker M, S\u00e1nchez C, Scheffel T, Schmitz M, Schramm A (2018) TeSSLa: runtime verification of non-synchronized real-time streams. In: Proceedings of the 33rd symposium on applied computing (SAC\u201918). ACM Press, New York, NY","DOI":"10.1145\/3167132.3167338"},{"key":"428_CR18","doi-asserted-by":"crossref","unstructured":"Gorostiaga F, S\u00e1nchez C (2018) Striver: stream runtime verification for real-time event-streams. In: Proceedings of the 18th international conference on runtime verification (RV\u201918). LNCS, vol 11237. Springer, Cham, pp 282\u2013298","DOI":"10.1007\/978-3-030-03769-7_16"},{"key":"428_CR19","doi-asserted-by":"crossref","unstructured":"Faymonville P, Finkbeiner B, Schledjewski M, Schwenger M, Stenger M, Tentrup L, Hazem T (2019) StreamLAB: stream-based monitoring of cyber-physical systems. In: Proceeings of the 31st international conference on computer-aided verification (CAV\u201919). LNCS, vol 11561. Springer, Cham, pp 421\u2013431","DOI":"10.1007\/978-3-030-25540-4_24"},{"key":"428_CR20","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10009-021-00605-3","volume":"23","author":"F Gorostiaga","year":"2021","unstructured":"Gorostiaga F, S\u00e1nchez C (2021) Stream runtime verification of real-time event-streams with the Striver language. Int J Softw Tools Technol Transf 23:157\u2013183","journal-title":"Int J Softw Tools Technol Transf"},{"key":"428_CR21","doi-asserted-by":"publisher","unstructured":"Gorostiaga F, S\u00e1nchez C (2021) HStriver: a very functional extensible tool for the runtime verification of real-time event streams. In: Proceedings of the 24th international symposium on formal methods (FM\u201921). LNCS, vol 13047. Springer, Cham, pp. 563\u2013580. https:\/\/doi.org\/10.1007\/978-3-030-90870-6_30","DOI":"10.1007\/978-3-030-90870-6_30"},{"issue":"2","key":"428_CR22","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10009-014-0309-2","volume":"17","author":"K Havelund","year":"2015","unstructured":"Havelund K (2015) Rule-based runtime verification revisited. Int J Softw Tools Technol Transf 17(2):143\u2013170","journal-title":"Int J Softw Tools Technol Transf"},{"key":"428_CR23","doi-asserted-by":"crossref","unstructured":"Barringer H, Havelund K (2011) TraceContract: a scala DSL for trace analysis. In: Proceedings of the 17th international symposium on formal methods (FM\u201911). LNCS, vol 6664. Springer, Heidelberg, pp. 57\u201372","DOI":"10.1007\/978-3-642-21437-0_7"},{"key":"428_CR24","first-page":"201","volume-title":"Electronic notes on theoretical computer science","author":"V Stolz","year":"2005","unstructured":"Stolz V, Huch F (2005) Runtime verification of concurrent Haskell programs. Electronic notes on theoretical computer science, vol 113. Elsevier, Amsterdam, pp 201\u2013216"},{"key":"428_CR25","doi-asserted-by":"crossref","unstructured":"Ceresa M, Gorostiaga F, S\u00e1nchez C (2020) Declarative stream runtime verification (hLola). In: Proc. of the 18th Asian Symposium on Programming Languages and Systems (APLAS\u201920). LNCS, vol 12470. Springer, Cham, pp 25\u201343","DOI":"10.1007\/978-3-030-64437-6_2"},{"key":"428_CR26","doi-asserted-by":"crossref","unstructured":"Falcone Y, Krstic S, Reger G, Traytel D (2018) A taxonomy for classifying runtime verification tools. In: Proceedings of the 18th international conference on runtime verification (RV\u201918). LNCS, vol 11237. Springer, Cham, pp 241\u2013262","DOI":"10.1007\/978-3-030-03769-7_14"},{"key":"428_CR27","doi-asserted-by":"crossref","unstructured":"Reinbacher T, Rozier KY, Schumann J (2014) Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings 20th International Confer on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914). LNCS, vol 8413. Springer, Heidelberg, pp 357\u2013372","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"428_CR28","doi-asserted-by":"crossref","unstructured":"Hall\u00e9 S (2016) When RV meets CEP. In: Proceedings of the 16th international conference on runtime verification (RV\u201916). LNCS, vol 10012. Springer, Cham, pp 68\u201391","DOI":"10.1007\/978-3-319-46982-9_6"},{"key":"428_CR29","unstructured":"Hall\u00e9 S, Khoury R (2017) Event stream processing with BeepBeep 3. In: Proceedings of the international workshop on competitions, usability, benchmarks, evaluation, and standardisation for runtime verification tools (RV-CUBES). Kalpa Publications in Computing. EasyChair, pp 81\u201388"},{"key":"428_CR30","doi-asserted-by":"crossref","unstructured":"Basin D, Harva M, Klaedtke F, Zalinescu E (2011) MONPOLY: monitoring usage-control policies. In: Proceedings of the 2nd international conference on runtime verification (RV\u201911). LNCS, vol 7186. Springer, Heidelberg, pp 360\u2013364","DOI":"10.1007\/978-3-642-29860-8_27"},{"key":"428_CR31","unstructured":"Basin DA, Klaedtke F, Zalinescu E (2017) The MonPoly monitoring tool. In: Proceedings of the international workshop on competitions, usability, benchmarks, evaluation, and standardisation for runtime verification tools (RV-CUBES). Kalpa Publications in Computing. EasyChair, pp 19\u201328"},{"key":"428_CR32","doi-asserted-by":"crossref","unstructured":"Pike L, Goodloe A, Morisset R, Niller S (2010) Copilot: a hard real-time runtime monitor. In: Proceedings of the 1st international conference on runtime verification (RV\u201910). LNCS, vol 6418. Springer, Heidelberg, pp 345\u2013359","DOI":"10.1007\/978-3-642-16612-9_26"},{"key":"428_CR33","unstructured":"Faymonville P, Finkbeiner B, Schwenger M, Torfah H(2017) Real-time stream-based monitoring. CoRR arXiv:1711.03829"},{"key":"428_CR34","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-319-89884-1_4","volume-title":"Programming languages and systems","author":"J Aguado","year":"2018","unstructured":"Aguado J, Mendler M, Pouzet M, Roop P, von Hanxleden R (2018) Deterministic concurrency: a clock-synchronised shared memory approach. In: Ahmed A (ed) Programming languages and systems. Springer, Cham, pp 86\u2013113"},{"key":"428_CR35","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-642-35722-0_24","volume-title":"Logical foundations of computer science","author":"J-P Talpin","year":"2013","unstructured":"Talpin J-P, Brandt J, Gem\u00fcnde M, Schneider K, Shukla S (2013) Constructive polychronous systems. In: Artemov S, Nerode A (eds) Logical foundations of computer science. Springer, Berlin, Heidelberg, pp 335\u2013349"},{"key":"428_CR36","unstructured":"Marlow S (2010) Haskell language report"},{"key":"428_CR37","doi-asserted-by":"crossref","unstructured":"Gorostiaga F, S\u00e1nchez C (2021) Nested monitors: monitors as expressions to build monitors. In: Proceedings of the 21st international conference on runtime verification (RV\u201921). LNCS, vol 12974. Springer, Heidelberg, pp 164\u2013183","DOI":"10.1007\/978-3-030-88494-9_9"},{"key":"428_CR38","unstructured":"Gorostiaga F (2022) Theory and practice of stream runtime verification for sequences and real-time event based systems. https:\/\/oa.upm.es\/70504\/"},{"key":"428_CR39","doi-asserted-by":"crossref","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Proceedings of the joint international conference on formal techniques, modelling and analysis of timed and fault-tolerant systems, and formal modelling and analysis of timed systems (FORMATS\/FTRTFT 2004). LNCS, vol 3253. Springer, Heidelberg, pp 152\u2013166","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"428_CR40","doi-asserted-by":"crossref","unstructured":"Donz\u00e9 A, Ferr\u00e8re T, Maler O (2013) Efficient robust monitoring for STL. In: Proceedings of the 25th international conference on computer aided verification (CAV\u201913). LNCS, vol 8044. Springer, Heidelberg, pp 264\u2013279","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"428_CR41","doi-asserted-by":"crossref","unstructured":"Jin X, Deshmukh JV, Kapinski J, Ueda K, Butts K (2014) Powertrain control verification benchmark. In: Proceedings of the 17th international conference on hybrid systems: computation and control (HSCC\u201914). ACM, New York, pp 253\u2013262","DOI":"10.1145\/2562059.2562140"},{"key":"428_CR42","doi-asserted-by":"crossref","unstructured":"Cumin J, Lefebvre G, Ramparany F, Crowley J (2017) A dataset of routine daily activities in an instrumented home. In: Proceedings of the 11th international conference on ubiquitous computing and ambient intelligence (UCAmI\u201917). LNCS, vol 10586. Springer, Cham, pp 413\u2013425","DOI":"10.1007\/978-3-319-67585-5_43"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00428-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00428-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00428-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T18:25:33Z","timestamp":1729621533000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00428-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["428"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00428-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2022,8]]},"assertion":[{"value":"29 April 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 April 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 June 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}