{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:42:23Z","timestamp":1761324143119,"version":"3.37.3"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,2,27]],"date-time":"2018-02-27T00:00:00Z","timestamp":1519689600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,2,27]],"date-time":"2018-02-27T00:00:00Z","timestamp":1519689600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-14-1-0261"],"award-info":[{"award-number":["FA9550-14-1-0261"]}],"id":[{"id":"10.13039\/100000181","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":[[2018,8]]},"DOI":"10.1007\/s10703-018-0317-z","type":"journal-article","created":{"date-parts":[[2018,2,27]],"date-time":"2018-02-27T16:32:39Z","timestamp":1519749159000},"page":"54-82","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Inferring event stream abstractions"],"prefix":"10.1007","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6341-3898","authenticated-orcid":false,"given":"Sean","family":"Kauffman","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7079-0472","authenticated-orcid":false,"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1413-0140","authenticated-orcid":false,"given":"Rajeev","family":"Joshi","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Fischmeister","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,2,27]]},"reference":[{"key":"317_CR1","unstructured":"Albarghouthi A, Baier JA, McIlraith SA (2009) On the use of planning technology for verification. In: Proceedings of the ICAPS workshop on verification & validation of planning & scheduling systems (VVPS), Citeseer"},{"issue":"11","key":"317_CR2","doi-asserted-by":"publisher","first-page":"832","DOI":"10.1145\/182.358434","volume":"26","author":"JF Allen","year":"1983","unstructured":"Allen JF (1983) Maintaining knowledge about temporal intervals. Commun ACM 26(11):832\u2013843","journal-title":"Commun ACM"},{"issue":"2","key":"317_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0004-3702(84)90008-0","volume":"23","author":"JF Allen","year":"1984","unstructured":"Allen JF (1984) Towards a general theory of action and time. Artif Intell 23(2):123\u2013154","journal-title":"Artif Intell"},{"key":"317_CR4","unstructured":"Alur R, Fisman D, Raghothaman M (2016) Regular programming for quantitative properties of data streams. In: Programming languages and systems\u201425th European symposium on programming, ESOP 2016, Eindhoven, The Netherlands. Springer, LNCS, vol 9632, pp 15\u201340"},{"issue":"2","key":"317_CR5","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/s00778-004-0147-z","volume":"15","author":"A Arasu","year":"2006","unstructured":"Arasu A, Babu S, Widom J (2006) The CQL continuous query language: semantic foundations and query execution. Int J Very Large Data Bases 15(2):121\u2013142","journal-title":"Int J Very Large Data Bases"},{"key":"317_CR6","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). Springer, LNCS, vol 6664, pp 57\u201372"},{"key":"317_CR7","doi-asserted-by":"crossref","unstructured":"Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: International conference on verification, model checking, and abstract interpretation (VMCAI), vol 2937, pp 44\u201357","DOI":"10.1007\/978-3-540-24622-0_5"},{"issue":"3","key":"317_CR8","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H Barringer","year":"2008","unstructured":"Barringer H, Rydeheard D, Havelund K (2008) Rule systems for run-time monitoring: from Eagle to RuleR. J Log Comput 20(3):675\u2013706","journal-title":"J Log Comput"},{"key":"317_CR9","doi-asserted-by":"publisher","unstructured":"Barringer H, Falcone Y, Havelund K, Reger G, Rydeheard D (2012) Quantified event automata: towards expressive and efficient runtime monitors. In: Proceedings of the 18th international symposium on formal methods (FM\u201912). Springer, pp 68\u201384. \n                    https:\/\/doi.org\/10.1007\/978-3-642-32759-9_9","DOI":"10.1007\/978-3-642-32759-9_9"},{"key":"317_CR10","unstructured":"Basin D, Harvan M, Klaedtke F, Z\u0103linescu E (2011) MONPOLY: monitoring usage\u2013control policies. In: 2nd international conference on runtime verification (RV\u201911). Springer, LNCS, vol 7186, pp 360\u2013364"},{"key":"317_CR11","doi-asserted-by":"crossref","unstructured":"Basin D, Klaedtke F, Marinovic S, Z\u0103linescu E (2015) Monitoring of temporal first-order properties with aggregations. Formal methods in system design. \n                    http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0222-7","DOI":"10.1007\/s10703-015-0222-7"},{"key":"317_CR12","unstructured":"Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly? In: 7th International workshop on runtime verification (RV\u201907). Springer, LNCS, vol 4839, pp 126\u2013138"},{"issue":"4","key":"317_CR13","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 (TOSEM) 20(4):14","journal-title":"ACM Trans Softw Eng Methodol (TOSEM)"},{"key":"317_CR14","unstructured":"Butler RW, Siminiceanu RI, Muno C (2007) The ANMLite language and logic for specifying planning problems. Report 215088:23681\u20132199"},{"key":"317_CR15","unstructured":"Chen F, Ro\u015fu G (2007) MOP: an efficient and generic runtime verification framework. In: ACM SIGPLAN notices. ACM, vol 42, pp 569\u2013588"},{"key":"317_CR16","unstructured":"CLIPS (2017) Website. \n                    http:\/\/clipsrules.sourceforge.net\n                    \n                  . Accessed 21 March 2017"},{"key":"317_CR17","doi-asserted-by":"publisher","unstructured":"Colombo C, Pace GJ, Schneider G (2009) Larva\u2014safer monitoring of real-time java programs (tool paper). In: Proceedings of the 2009 seventh IEEE international conference on software engineering and formal methods. IEEE Computer Society, Washington, DC, USA, SEFM \u201909, pp 33\u201337. \n                    https:\/\/doi.org\/10.1109\/SEFM.2009.13","DOI":"10.1109\/SEFM.2009.13"},{"key":"317_CR18","doi-asserted-by":"crossref","unstructured":"Cranor C, Johnson T, Spataschek O, Shkapenyuk V (2003) Gigascope: a stream database for network applications. In: Proceedings of the 2003 ACM SIGMOD international conference on management of data. ACM, pp 647\u2013651","DOI":"10.1145\/872757.872838"},{"issue":"3","key":"317_CR19","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/2187671.2187677","volume":"44","author":"G Cugola","year":"2012","unstructured":"Cugola G, Margara A (2012) Processing flows of information: from data stream to complex event processing. ACM Comput Surv (CSUR) 44(3):15","journal-title":"ACM Comput Surv (CSUR)"},{"key":"317_CR20","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 on temporal representation and reasoning. IEEE Computer Society, pp 166\u2013174","DOI":"10.1109\/TIME.2005.26"},{"key":"317_CR21","doi-asserted-by":"publisher","unstructured":"Decker N, Leucker M, Thoma D (2013) jUnitRV\u2014adding runtime verification to jUnit. In: Brat G, Rungta N, Venet A (eds) NASA formal methods, 5th international symposium, NFM 2013, Moffett Field, CA, USA, May 14\u201316, 2013. Proceedings. Springer, Lecture Notes in Computer Science, vol 7871, pp 459\u2013464. \n                    https:\/\/doi.org\/10.1007\/978-3-642-38088-4_34","DOI":"10.1007\/978-3-642-38088-4_34"},{"issue":"2","key":"317_CR22","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10009-015-0380-3","volume":"18","author":"N Decker","year":"2016","unstructured":"Decker N, Leucker M, Thoma D (2016) Monitoring modulo theories. Int J Softw Tools Technol Transf 18(2):205\u2013225. \n                    https:\/\/doi.org\/10.1007\/s10009-015-0380-3","journal-title":"Int J Softw Tools Technol Transf"},{"key":"317_CR23","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/192218.192226","volume":"3","author":"LK Dillon","year":"1994","unstructured":"Dillon LK, Kutty G, Moser LE, Melliar-Smith PM, Ramakrishna YS (1994) A graphical interval logic for specifying concurrent systems. ACM Trans Softw Eng Methodol 3:131\u2013165","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"317_CR24","unstructured":"Doorenbos RB (1995) Production matching for large learning systems. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA, USA"},{"key":"317_CR25","unstructured":"Drools (2017) Website. \n                    http:\/\/www.jboss.org\/drools\n                    \n                  . Accessed 21 March 2017"},{"issue":"2","key":"317_CR26","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s00287-009-0329-6","volume":"32","author":"M Eckert","year":"2009","unstructured":"Eckert M, Bry F (2009) Complex event processing (CEP). Informatik-Spektrum 32(2):163\u2013167","journal-title":"Informatik-Spektrum"},{"issue":"1","key":"317_CR27","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C (2007) The Daikon system for dynamic detection of likely invariants. Sci Comput Progr 69(1):35\u201345","journal-title":"Sci Comput Progr"},{"key":"317_CR28","doi-asserted-by":"publisher","unstructured":"Falcone Y, Havelund K, Reger G (2013) A tutorial on runtime verification. In: Engineering dependable software systems, pp 141\u2013175. \n                    https:\/\/doi.org\/10.3233\/978-1-61499-207-3-141","DOI":"10.3233\/978-1-61499-207-3-141"},{"issue":"3","key":"317_CR29","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10703-005-3399-3","volume":"27","author":"B Finkbeiner","year":"2005","unstructured":"Finkbeiner B, Sankaranarayanan S, Sipma H (2005) Collecting statistics over runtime executions. Form Methods Syst Des 27(3):253\u2013274","journal-title":"Form Methods Syst Des"},{"key":"317_CR30","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(82)90020-0","volume":"19","author":"C Forgy","year":"1982","unstructured":"Forgy C (1982) Rete: a fast algorithm for the many pattern\/many object pattern match problem. Artif Intell 19:17\u201337","journal-title":"Artif Intell"},{"key":"317_CR31","unstructured":"Goubault-Larrecq J, Olivain J (2008) A smell of ORCHIDS. In: Proceedings of the 8th international workshop on runtime verification (RV\u201908). Springer, LNCS, vol 5289, pp 1\u201320"},{"key":"317_CR32","doi-asserted-by":"crossref","unstructured":"Hall\u00e9 S (2016) When RV, Meets CEP. In: Runtime verification: Proceedings of 16th international conference, RV 2016, Madrid, Spain, September 23\u201330, 2016. Springer, pp 68\u201391","DOI":"10.1007\/978-3-319-46982-9_6"},{"key":"317_CR33","unstructured":"Hall\u00e9 S, Gaboury S, Bouchard B (2016) Activity recognition through complex event processing: first findings. In: AAAI workshop: artificial intelligence applied to assistive technologies and smart environments"},{"key":"317_CR34","doi-asserted-by":"crossref","unstructured":"Hansen MR, Van\u00a0Hung D (2007) A theory of duration calculus with application. In: Domain modeling and the duration calculus, LNCS, vol 4710. Springer, pp 119\u2013176","DOI":"10.1007\/978-3-540-74964-6_3"},{"issue":"2","key":"317_CR35","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":"317_CR36","unstructured":"Havelund K, Joshi R (2014) Comprehension of spacecraft telemetry using hierarchical specifications of behavior. In: Merz S, Pang J (eds) Formal methods and software engineering: 16th international conference on formal engineering methods, ICFEM 2014, Luxembourg, November 3\u20135, 2014. Proceedings. Springer International Publishing, LNCS, vol 8829, pp 187\u2013202"},{"key":"317_CR37","doi-asserted-by":"crossref","unstructured":"Havelund K, Joshi R (2015) Experience with rule-based analysis of spacecraft logs. In: Artho C, \u00d6lveczky CP (eds) Formal techniques for safety-critical systems: third international workshop (FTSCS 2014), November 2014, Luxembourg. Springer International Publishing, Communications in Computer and Information Science, vol 476, pp 1\u201316","DOI":"10.1007\/978-3-319-17581-2_1"},{"key":"317_CR38","doi-asserted-by":"crossref","unstructured":"Havelund K, Peled D, Ulus D (2017) First order temporal logic monitoring with BDDs. 17th Conference on formal methods in computer-aided design (FMCAD 2017), 2\u20136 October, Austria. IEEE Computer Society, Vienna, pp 116\u2013123","DOI":"10.23919\/FMCAD.2017.8102249"},{"key":"317_CR39","unstructured":"Jess (2017) Website. \n                    http:\/\/www.jessrules.com\/jess\n                    \n                  . Accessed 21 March 2017"},{"key":"317_CR40","unstructured":"Kauffman S, Havelund K, Joshi R (2016) nfer\u2014a notation and system for inferring event stream abstractions. In: Falcone Y, S\u00e1nchez C (eds) Runtime verification: 16th international conference, RV 2016, Madrid, Spain, September 23\u201330, 2016, Proceedings. Springer, LNCS, vol 10012, pp 235\u2013250"},{"issue":"8","key":"317_CR41","doi-asserted-by":"publisher","first-page":"787","DOI":"10.1002\/spe.4380210803","volume":"21","author":"SM Kearns","year":"1991","unstructured":"Kearns SM (1991) Extending regular expressions with context operators and parse extraction. Softw Pract Exp 21(8):787\u2013804. \n                    https:\/\/doi.org\/10.1002\/spe.4380210803","journal-title":"Softw Pract Exp"},{"key":"317_CR42","unstructured":"Kreps J, Narkhede N, Rao J (2011) Kafka: a distributed messaging system for log processing. In: Proceedings of the 6th international workshop on networking meets databases (NetDB\u201911). ACM, pp 1\u20137"},{"key":"317_CR43","doi-asserted-by":"crossref","unstructured":"Legay A, Delahaye B, Bensalem S (2010) Statistical model checking: an overview. In: 1st international conference on runtime verification (RV\u201910). Springer, LNCS, vol 6418","DOI":"10.1007\/978-3-642-16612-9_11"},{"issue":"5","key":"317_CR44","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. \n                    https:\/\/doi.org\/10.1016\/j.jlap.2008.08.004","journal-title":"J Log Algebr Program"},{"key":"317_CR45","volume-title":"The power of events: an introduction to complex event processing in distributed enterprise systems","author":"D Luckham","year":"2002","unstructured":"Luckham D (2002) The power of events: an introduction to complex event processing in distributed enterprise systems. Addison-Wesley, Boston"},{"key":"317_CR46","unstructured":"Mcdermott D, Ghallab M, Howe A, Knoblock C, Ram A, Veloso M, Weld D, Wilkins D (1998) PDDL\u2014the planning domain definition language. Tech. rep., CVC TR-98-003\/DCS TR-1165, Yale Center for Computational Vision and Control"},{"key":"317_CR47","doi-asserted-by":"publisher","unstructured":"Meredith P, Jin D, Griffith D, Chen F, Ro\u015fu G (2011) An overview of the MOP runtime verification framework. Int J Softw Tools Technol Transf. \n                    https:\/\/doi.org\/10.1007\/s10009-011-0198-6","DOI":"10.1007\/s10009-011-0198-6"},{"key":"317_CR48","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"BC Moszkowski","year":"1985","unstructured":"Moszkowski BC (1985) A temporal logic for multilevel reasoning about hardware. IEEE Comput 18:10\u201319","journal-title":"IEEE Comput"},{"key":"317_CR49","unstructured":"Narayan A, Kauffman S, Morgan J, Tchamgoue GM, Joshi Y, Hobbs C, Fischmeister S (2017) System call logs with natural random faults: experimental design and application. In: SELSE-13: the 13th workshop on silicon errors in logic, system effects, Boston, MA, USA"},{"key":"317_CR50","doi-asserted-by":"crossref","unstructured":"Navabpour S, Joshi Y, Wu W, Berkovich S, Medhat R, Bonakdarpour B, Fischmeister S (2013) RiTHM: a tool for enabling time-triggered runtime verification for C programs. In: Proceedings of the 2013 9th joint meeting on foundations of software engineering. ACM, pp 603\u2013606","DOI":"10.1145\/2491411.2494596"},{"key":"317_CR51","volume-title":"QNX operating system: system architecture","author":"QNX","year":"1997","unstructured":"QNX (1997) QNX operating system: system architecture. QNX Software Systems Ltd, Ontario"},{"key":"317_CR52","unstructured":"R Development Core Team (2008) R: A Language and Environment for Statistical Computing. R Foundation for Statistical Computing, Vienna, Austria. ISBN: 3-900051-07-0. \n                    http:\/\/www.R-project.org"},{"key":"317_CR53","unstructured":"Reger G (2014) Automata based monitoring and mining of execution traces. Ph.D. thesis, University of Manchester"},{"key":"317_CR54","doi-asserted-by":"crossref","unstructured":"Reger G, Cruz HC, Rydeheard D (2015) MarQ: monitoring at runtime with QEA. In: Proceedings of the 21st international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201915)","DOI":"10.1007\/978-3-662-46681-0_55"},{"key":"317_CR55","unstructured":"Rosu G, Bensalem S (2006) Allen linear (interval) temporal logic\u2014translation to LTL and monitor synthesis. In: 18th international conference on computer aided verification (CAV\u201906). Springer, LNCS, vol 4144, pp 263\u2013277"},{"key":"317_CR56","doi-asserted-by":"crossref","unstructured":"Siminiceanu R, Butler RW, Mu\u00f1oz CA (2009) Experimental evaluation of a planning language suitable for formal verification. In: 5th international workshop on model checking and artificial intelligence (MoChArt\u201908), LNCS, vol 5348. Springer, pp 132\u2013146","DOI":"10.1007\/978-3-642-00431-5_9"},{"key":"317_CR57","unstructured":"Xilinx (2017) Zynq-7000 all programmable soc zc706 evaluation kit. \n                    https:\/\/www.xilinx.com\/products\/boards-and-kits\/ek-z7-zc706-g.html\n                    \n                  . Accessed 13 March 2017"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-0317-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0317-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0317-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:46:19Z","timestamp":1589730379000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-0317-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,27]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["317"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-0317-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2018,2,27]]},"assertion":[{"value":"27 February 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}