{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,4]],"date-time":"2024-08-04T08:10:38Z","timestamp":1722759038254},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"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":["Software Qual J"],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study the problem of online runtime verification of real-time event streams. Our monitors can observe concurrent systems with a shared clock, but where each component reports observations as signals that arrive to the monitor at different speeds and with different and varying latencies. We start from specifications in a fragment of the TeSSLa specification language, where streams (including inputs and final verdicts) are not restricted to be Booleans but can be data from richer domains, including integers and reals with arithmetic operations and aggregations. Specifications can be used both for checking logical properties and for computing statistics and general numeric temporal metrics (and properties on these richer metrics). We present an online evaluation algorithm for the specification language and a concurrent implementation of the evaluation algorithm. The algorithm can tolerate and exploit the asynchronous arrival of events without synchronizing the inputs. Then, we introduce a theory of asynchronous transducers and show a formal proof of the correctness such that every possible run of the monitor implements the semantics. Finally, we report an empirical evaluation of a highly concurrent Erlang implementation of the monitoring algorithm.<\/jats:p>","DOI":"10.1007\/s11219-019-09493-y","type":"journal-article","created":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T09:02:29Z","timestamp":1587200549000},"page":"745-787","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Runtime verification of real-time event streams under non-synchronized arrival"],"prefix":"10.1007","volume":"28","author":[{"given":"Martin","family":"Leucker","sequence":"first","affiliation":[]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[]},{"given":"Torben","family":"Scheffel","sequence":"additional","affiliation":[]},{"given":"Malte","family":"Schmitz","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Schramm","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"9493_CR1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"Actors: a model of concurrent computation in distributed systems","author":"G Agha","year":"1986","unstructured":"Agha, G. (1986). Actors: a model of concurrent computation in distributed systems. Cambridge: MIT Press."},{"key":"9493_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Feder, T., & Henzinger, T.A. (1996). The benefits of relaxing punctuality. Journal of the ACM.","DOI":"10.1145\/227595.227602"},{"issue":"2","key":"9493_CR3","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/506147.506151","volume":"49","author":"E Asarin","year":"2002","unstructured":"Asarin, E., Caspi, P., & Maler, O. (2002). Timed regular expressions. Journal of the ACM, 49(2), 172\u2013206.","journal-title":"Journal of the ACM"},{"key":"9493_CR4","unstructured":"Barringer, H., Goldberg, A., Havelund, K., & Sen, K. (2004). Rule-based runtime verification. In Proc. of VMCAI\u201904, LNCS 2937 (pp. 44\u201357): Springer."},{"key":"9493_CR5","doi-asserted-by":"crossref","unstructured":"Bartocci, E., & Falcone, Y. (Eds.). (2018). Lectures on runtime verification - introductory and advanced topics, LNCS, Vol. 10457. Berlin: Springer.","DOI":"10.1007\/978-3-319-75632-5"},{"issue":"4","key":"9493_CR6","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 Transactions on Software Engineering and Methodology, 20(4), 14.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"9493_CR7","unstructured":"Bauer, A., K\u00fcster, J. C., & Vegliach, G. (2013). From propositional to first-order monitoring. In Proc. of RV\u201913, LNCS, (Vol. 8174 pp. 59\u201375): Springer."},{"key":"9493_CR8","doi-asserted-by":"crossref","unstructured":"Baumeister, J., Finkbeiner, B., Schwenger, M., & Torfah, H. (2019). Fpga stream-monitoring of real-time properties. In EMSOFT. ACM.","DOI":"10.1145\/3358220"},{"key":"9493_CR9","doi-asserted-by":"crossref","first-page":"425","DOI":"10.7551\/mitpress\/5641.003.0021","volume-title":"Proof, language, and interaction: essays in honour of Robin Milner, chap. The foundations of Esterel","author":"G Berry","year":"2000","unstructured":"Berry, G. (2000). Proof, language, and interaction: essays in honour of Robin Milner, chap. The foundations of Esterel, (pp. 425\u2013454). Cambridge: MIT Press."},{"key":"9493_CR10","unstructured":"Bozelli, L., & S\u00e1nchez, C. (2014). Foundations of Boolean stream runtime verification. In In Proc. RV\u201914, LNCS, (Vol. 8734 pp. 64\u201379): Springer."},{"key":"9493_CR11","unstructured":"Caspi, P., & Pouzet, M. (1996). Synchronous Kahn Networks. In Proc. of ICFP\u201996 (pp. 226\u2013238): ACM Press."},{"issue":"4","key":"9493_CR12","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s004460050049","volume":"11","author":"CM Chase","year":"1998","unstructured":"Chase, C.M., & Garg, V.K. (1998). Detection of global predicates: techniques and their limitations. Distributed Computing, 11(4), 191\u2013201.","journal-title":"Distributed Computing"},{"key":"9493_CR13","unstructured":"Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., & Thoma, D. (2018). Tessla: temporal stream-based specification language. In Formal methods: foundations and applications - 21th Brazilian symposium, SBMF 2018, Recife, Brazil, November 26 - November 30, 2018. Proceedings lecture notes in computer science: Springer."},{"issue":"6","key":"9493_CR14","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1109\/71.774912","volume":"10","author":"F Cristian","year":"1999","unstructured":"Cristian, F., & Fetzer, C. (1999). The timed asynchronous distributed system model. IEEE Transactions on Parallel and Distributed Systems, 10(6), 642\u2013657.","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"9493_CR15","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., & Manna, Z. (2005). LOLA: runtime monitoring of synchronous systems. In Proc. of TIME\u201905 (pp. 166\u2013174): IEEE."},{"key":"9493_CR16","unstructured":"Decker, N., Gottschling, P., Hochberger, C., Leucker, M., Scheffel, T., Schmitz, M., & Weiss, A. (2017). Rapidly adjustable non-intrusive online monitoring for multi-core systems. In 20th Brazilian symposium on formal methods (SBMF 2017): Springer."},{"key":"9493_CR17","unstructured":"Decker, N., Dreyer, B., Gottschling, P., Hochberger, C., Lange, A., Leucker, M., Scheffel, T., Wegener, S., & Weiss, A. (2018). Online analysis of debug trace data for embedded systems. In DATE: IEEE."},{"key":"9493_CR18","unstructured":"Donz\u00e9, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., & Smolka, S.A. (2012). On temporal logic and signal processing. In In Proc. of ATVA\u201912, LNCS, (Vol. 7561 pp. 92\u2013106): Springer."},{"key":"9493_CR19","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., & Campenhout, D.V. (2003). Reasoning with temporal logic on truncated paths. In Proc. of CAV\u201903, LNCS 2725, (Vol. 2725 pp. 27\u201339): Springer."},{"key":"9493_CR20","unstructured":"Eliot, C., & Hudak, P. (1997). Functional reactive animation. In Proc. of ICFP\u201907 (pp. 163\u2013173): ACM."},{"key":"9493_CR21","doi-asserted-by":"publisher","unstructured":"Faymonville, P., Finkbeiner, B., Schirmer, S., & Torfah, H. (2016). A stream-based specification language for network monitoring. In Proc. of the 16th Int\u2019l conf. on runtime verification (RV\u201916), LNCS, (Vol. 10012 pp. 152\u2013168): Springer, DOI https:\/\/doi.org\/10.1007\/978-3-319-46982-9_10.","DOI":"10.1007\/978-3-319-46982-9_10"},{"key":"9493_CR22","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 Proc. of the 31st Int\u2019l conf. on computer-aided verification (CAV\u201919), LNCS, (Vol. 11561 pp. 421\u2013431): Springer."},{"key":"9493_CR23","unstructured":"Gautier, T., Le Guernic, P., & Besnard, L. (1987). SIGNAL: a declarative language for synchronous programming of real-time systems. In Proc. of FPCA\u201987, LNCS 274 (pp. 257\u2013277): Springer."},{"key":"9493_CR24","unstructured":"Goodloe, A.E., & Pike, L. (2010). Monitoring distributed real-time systems: a survey and future directions. Tech. rep., NASA Langley Research Center."},{"key":"9493_CR25","unstructured":"Gorostiaga, F., & S\u00e1nchez, C. (2018). Striver: Stream runtime verification for real-time event-streams. In Proc. of the 18th int\u2019l conf on runtime verification (RV\u201918), LNCS, (Vol. 11237 pp. 282\u2013298): Springer."},{"key":"9493_CR26","unstructured":"Halbwachs, N., Caspi, P., Pilaud, D., & Plaice, J. (1987). Lustre: a declarative language for programming synchronous systems. In Proc. of POPL\u201987 (pp. 178\u2013188): ACM Press."},{"key":"9493_CR27","unstructured":"Havelund, K., & Goldberg, A. (2005). Verify your runs. In Proc. of VSTTE\u201905, LNCS 4171 (pp. 374\u2013383): Springer."},{"key":"9493_CR28","unstructured":"Havelund, K., & Ro\u015fu, G. (2002). Synthesizing monitors for safety properties. In Proc. of TACAS\u201902, LNCS 2280 (pp. 342\u2013356): Springer."},{"key":"9493_CR29","unstructured":"Hewitt, C., Bishop, P., & Steiger, R. (1973). A universal modular ACTOR formalism for artificial intelligence. IJCAI, 235\u2013245."},{"key":"9493_CR30","doi-asserted-by":"crossref","unstructured":"Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., & Nickovic, D. (2015). From signal temporal logic to FPGA monitors. In Proc. of MEMOCODE 2015 (pp. 218\u2013227).","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"9493_CR31","unstructured":"Jaksic, S., Bartocci, E., Grosu, R., & Nickovic, D. (2016). Quantitative monitoring of STL with edit distance. In Prov. of RV\u201916, LNCS, (Vol. 10012 pp. 201\u2013218)."},{"key":"9493_CR32","unstructured":"Leucker, M. (2011). Teaching runtime verification. In Proc. of RV\u201911, no. 7186 in LNCS (pp. 34\u201348): Springer."},{"issue":"5","key":"9493_CR33","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. Logic Algebr. Progr., 78(5), 293\u2013303.","journal-title":"J. Logic Algebr. Progr."},{"key":"9493_CR34","unstructured":"Leucker, M., S\u00e1nchez, C., Scheffel, T., Schmitz, M., & Schramm, A. (2018). TeSSLa: runtime verification of non-synchronized real-time streams. In Proc. of the 33rd symposium on applied computing (SAC\u201918): ACM."},{"key":"9493_CR35","doi-asserted-by":"crossref","unstructured":"Maler, O., & Nickovic, D. (2004). Monitoring temporal properties of continuous signals. In FTRTFT (pp. 152\u2013166).","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"9493_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., & Pnueli, A. (1995). Temporal verification of reactive systems: safety. New York: Springer."},{"key":"9493_CR37","unstructured":"Pike, L., Goodloe, A., Morisset, R., & Niller, S. (2010). Copilot: a hard real-time runtime monitor. In Proc. of RV\u201910, LNCS 6418: Springer."},{"key":"9493_CR38","unstructured":"Pnueli, A., & Zaks, A. (2006). PSL model checking and run-time verification via testers. In Proc. of FM\u201906, LNCS 4085 (pp. 573\u2013586): Springer."},{"key":"9493_CR39","unstructured":"Reinbacher, T., Rozier, K.Y., & Schumann, J. (2014). Temporal-logic based runtime observer pairs for system health management of real-time systems. In Proc. of the 20th Int\u2019l conf. on tools and algorithms for the construction and analysis of systems (TACAS\u201914), no. 8413 in LNCS (pp. 357\u2013372): Springer."},{"issue":"2","key":"9493_CR40","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. Automated Software Engineering, 12(2), 151\u2013197.","journal-title":"Automated Software Engineering"},{"key":"9493_CR41","unstructured":"S\u00e1nchez, C. (2018). Online and offline stream runtime verification of synchronous systems. In Proc. of the 18th Int\u2019l conf. on runtime verification (RV\u201918), LNCS, (Vol. 11237 pp. 138\u2013163): Springer."},{"key":"9493_CR42","doi-asserted-by":"crossref","unstructured":"Selyunin, K., Nguyen, T., Bartocci, E., & Grosu, R. (2016). Applying runtime monitoring for automotive electronic development. In Proc. of RV\u201916, LNCS, (Vol. 10012 pp. 462\u2013469).","DOI":"10.1007\/978-3-319-46982-9_30"},{"key":"9493_CR43","unstructured":"Selyunin, K., Jaksic, S., Nguyen, T., Reidl, C., Hafner, U., Bartocci, E., Nickovic, D., & Grosu, R. (2017). Runtime monitoring with recovery of the sent communication protocol. In Proc. of CAV\u201917, LNCS, (Vol. 10426 pp. 336\u2013355): Springer."},{"issue":"2","key":"9493_CR44","first-page":"226","volume":"89","author":"K Sen","year":"2003","unstructured":"Sen, K., & Ro\u015fu, G. (2003). Generating optimal monitors for extended regular expressions. ENTCS, 89(2), 226\u2013245.","journal-title":"ENTCS"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-019-09493-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11219-019-09493-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-019-09493-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,4]],"date-time":"2024-08-04T07:25:49Z","timestamp":1722756349000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11219-019-09493-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,18]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["9493"],"URL":"https:\/\/doi.org\/10.1007\/s11219-019-09493-y","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"type":"print","value":"0963-9314"},{"type":"electronic","value":"1573-1367"}],"subject":[],"published":{"date-parts":[[2020,4,18]]},"assertion":[{"value":"18 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}