{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T11:10:07Z","timestamp":1748430607205,"version":"3.41.0"},"publisher-location":"Wiesbaden","reference-count":60,"publisher":"Springer Fachmedien Wiesbaden","isbn-type":[{"type":"print","value":"9783658099930"},{"type":"electronic","value":"9783658099947"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-658-09994-7_6","type":"book-chapter","created":{"date-parts":[[2015,6,5]],"date-time":"2015-06-05T07:56:17Z","timestamp":1433490977000},"page":"151-189","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Specification of Parametric Monitors"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,6,6]]},"reference":[{"key":"6_CR1","unstructured":"RuleR website. http:\/\/www.CB.man.ac.uk\/~howard\/LPA.html."},{"key":"6_CR2","unstructured":"CSRV 2of4. http:\/\/rv2014.imag.fr\/monitoring-competition."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"C. Allan, P. Avgustinov, A. S. Christensen, L. Hendren, S. Kuzins, O. Lhot8.k, O. de Moor, D. Sereni, G. Sittamplao, aod J. Tibble. Adding trace matching with free variables to AspectJ. In OOPSLA '05. ACM Press, 2005.","DOI":"10.1145\/1094811.1094839"},{"key":"6_CR4","unstructured":"H. Barringer, Y. Faleone, K. Havelund, G. Reger, and D. Rydeheard. Quaotified Event Automata \u2013 towards expressive and efficient runtime monitors. In 18 th International Symposium on Formal Methoos (FM'12), Paris, F'rance, August 27- 91, 2offt. Proceedings, volume\u00a07436 of LNCS. Springer, 2of2."},{"issue":"5","key":"6_CR5","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/BF01211631","volume":"7","author":"H. Barringer","year":"1995","unstructured":"H. Barringer, M. Fisher, D. M. Gabbay, G. Gough, and R. Owens. Metatem: An introduction. Formal Asp. Comput., 7(5):533\u2013549, 1995.","journal-title":"Formal Asp. Comput."},{"key":"6_CR6","unstructured":"H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Program monitoring with LTL in Eagle. In Parallel and Distributed Systems: Testing and Debugging (PAD TAD' 04), Santa Fee, New Mexico , USA, volume 17 of IEEE Computer Society , April 2004."},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-based runtbne verifieation. In VMCAI, volume\u00a02937 of LNCS, pages 44\u201357. Springer, 2004.","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"H. Barringer, A. Groce, K. Havelund, and M. Srnitb. Formal analysis of log files. Journal of Aerospace Computing, Information, and Communication, 7(11):365- 390,2of0.","DOI":"10.2514\/1.49356"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"H. Barringer and K. Havelund. TraceContract: A Scala DSL far trace analysis. In 17th International Symposium on Formal Methods (FM'l1), Limerick, Ireland, June 20-24, 2011. Proceedings, volume\u00a06664 of LNCS, pages 57-72. Springer, 2ofl.","DOI":"10.1007\/978-3-642-21437-0_7"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"H. Barringer, K. Havelund, D. Rydeheard, and A. Grace. Rule systems far runtime verification: A short tutorial. In Proc . of the 9th Int. Workshop on Runtime Verificotion (RV'09), volume\u00a05779 of LNCS, pages 1-24. Springer, 2009.","DOI":"10.1007\/978-3-642-04694-0_1"},{"key":"6_CR11","volume-title":"Rule systems for run-time monitoring: from Eagle to RuleR. In Proc. of the 7th Int. Workshop on Runtime Verificotion (RV'07), volume\u00a04839 of LNCS, pages 111-125, Vaneouver","author":"H. Barringer","year":"2007","unstructured":"H. Barringer, D. Rydeheard, and K. Havelund. Rule systems for run-time monitoring: from Eagle to RuleR. In Proc . of the 7th Int. Workshop on Runtime Verificotion (RV'07), volume\u00a04839 of LNCS, pages 111-125, Vaneouver, Canada, 2007. Springer."},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"H. Barringer, D. E. Rydeheard, and K. Havelund. Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput., 20(3):675-706, 2of0.","DOI":"10.1093\/logcom\/exn076"},{"key":"6_CR13","unstructured":"D. A. Basin, F. K1aedtke, and S. M\u00fcller. Poliey monitoring in first-order temporal logic. In T. Touili, B. Cook, and P. Jackson, editors, Computer Aided Verification , 22nd International Con\/erence, CA V 2of0, Edinburgh, UK, July 15-19, Proceedings, volume\u00a06174 of LNCS, pages 1-18. Springer, 2of0."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"A. Bauer, J.-C. K\u00fcster, and G. Vegliach. From propositional to first-order monitoring. In Runtime Verification - 4th Int. Conference, RV'19, Rennes, France , September 24-27, 2013. Proeeedings, volume\u00a08174 of LNCS, pages 59-75. Springer, 2013.","DOI":"10.1007\/978-3-642-40787-1_4"},{"key":"6_CR15","first-page":"126","volume-title":"Scba1lhart. The good, the bad, and the ugly, but how ngly is ngly? In Proe. of the 7th Int. Workshop on Runtime Verificotion (RV'07), volume\u00a04839 of LNCS","author":"A. Bauer","year":"2007","unstructured":"A. Bauer, M. Leucker, and C. Scba1lhart. The good, the bad, and the ugly, but how ngly is ngly? In Proe. of the 7th Int. Workshop on Runtime Verificotion (RV'07), volume\u00a04839 of LNCS, pages 126\u2013138, Vancouver, Canada, 2007. Springer."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"A. Bauer, M. Leucker, and J. Streit. SALT \u2013 struetured assertion language for temporallogic. In Z. Liu and J. He, editors, Formal Methods and Software Engineering , volume\u00a04260 of Lecture Notes in Computer Seieneo, pages 757\u2013775. Springer Berlin Heidelberg, 2006.","DOI":"10.1007\/11901433_41"},{"key":"6_CR17","unstructured":"E. Bodden. MOPBox: A library approach to runtime verifieation. In Runtime Verification - 2nd Int. Conference, RV'll, San Francisco, USA, September 27-90 , 2011. Proceedings, volume\u00a07186 of LNCS, pages 36 & -369. Springer, 201l."},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"F. Chen and G. Ro\u00a7u. Parametrie trace slicing and monitoring. In Proceedings of the 15th International Con\/erenee on Tools and Algorithms \/or the Construetion and Analysis of Systems (TACAS'09), volume\u00a05505 of LNCS, pages 246\u2013261, 2009.","DOI":"10.1007\/978-3-642-00768-2_23"},{"key":"6_CR19","unstructured":"Clips website: http:\/\/clipsrules.sourceforge.net."},{"key":"6_CR20","unstructured":"H. C. Cruz. Optimisation techniques for runtime verification. Master's thesis, University of Manchester, 2of4."},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"M. D' Amorim and K. Havelund. Event-based runtime verification of Java programs. In Workshop on Dynamie Program Analysis (WODA '05), volume 30(4) of ACM Sigsoft Software Engineering Notes, pages 1\u20137, 2005.","DOI":"10.1145\/1082983.1083249"},{"key":"6_CR22","unstructured":"N. Decker, M. Leucker, and D. Thoma. Monitoring modulo theories. In E. Abraham and K. Havelund, editors, Tools and Algorithms \/or the Constmetion and Analysis of Systems \u2013 20th International Con\/erenee, TACAS 2of4, Grenoble, F'rnnce, April 7-11, 2of4. Proceedings, volume\u00a08413 of LNCS, pages 341-356. Springer, 2of4."},{"key":"6_CR23","volume-title":"Production Matching for Large Leaming Systems. PhD thesis","author":"R. B. Doorenbos","year":"1995","unstructured":"R. B. Doorenbos. Production Matching for Large Leaming Systems. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, 1995."},{"key":"6_CR24","unstructured":"Droola website: http:\/\/www.jboss.org\/droola."},{"key":"6_CR25","unstructured":"Droola functional programming extensions website: https:\/\/eommurdty.jboss.org\/wiki\/FunctionaiProgrammingInDrools."},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"D. Drusinsky. The temporal rover and the ATG rover. In SPIN Model Checking and Software Verijiootion, volume\u00a01885 of LNCS, pages 323-330. Springer, 2000.","DOI":"10.1007\/10722468_19"},{"key":"6_CR27","unstructured":"D. Drusinsky. Modeling and Verijiootion using UML Statecharts. Elsevier, 2006. ISBN-13: 978-0-7506-7949-7, 400 pages."},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Y. Falcone, J.-C. Fernandez, and L. Mounier. Runtime verification of safetyprogress properties. In Proc. of the 9th Int. Workshop on Runtime Verijication (RV'09), volume\u00a05779 of LNCS, pages 40-59. Springer, 2009.","DOI":"10.1007\/978-3-642-04694-0_4"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Y. Falcone, J.-C. Fernandez, and L. Mounier. What can you verify and enforce at runtime? J Software Tools for Technology Transfer, 14(3):349-382, 2of2.","DOI":"10.1007\/s10009-011-0196-8"},{"key":"6_CR30","unstructured":"Y. Falcone, K. Havelund, and G. Reger. A tutorial on runtime verification. In M. Broy and D. Peled, editors, Summer School Marktoberdorf 2of2 \u2013 Engineering Dependable Software Systems, to appear . lOS Press, 2013."},{"key":"6_CR31","first-page":"17","volume":"19","author":"C. Forgy","year":"1982","unstructured":"C. Forgy. R.ete: A fast algorithm for the many pattern\/many object pattern match problem. Artijiciallntelligence, 19:17\u201337, 1982.","journal-title":"Artijiciallntelligence"},{"key":"6_CR32","unstructured":"M. Fusco. Hammurabi \u2013 a Scala rule engine. In Scala Days 2011, Stanford University, California, 2011."},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-th \u2026 fly automatie verification of linear temporallogic. fu P. Dembinski and M. Sredniawa, editors, In Protocol Specijication Testing and Verijication (PSTV), volume\u00a038, pages 3\u201318. Chapman & Hall, 1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"J. Goubault-Larrecq and J. Olivain. A smell of ORCHIDS. In Proc. of the 8th Int. Workshop on Runtime Verijiootion (RV'08), volume\u00a05289 of LNCS, pages 1-20, Budapest, Hungary, 2008. Springer.","DOI":"10.1007\/978-3-540-89247-2_1"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"A. Groce, K. Havelund, and M. H. Smith. From scripts to specifications: the evolution of a \u00dfight software testing effort. In 92nd Int. Conference on Software Engineering (ICSE'10), Cape Town, South Ajrioo, ACM SIG, pages 129-138, 2of0.","DOI":"10.1145\/1810295.1810314"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"S. Halle and R. Villemaire. Runtime enforcem.ent of web service message contracts with data. IEEE Transactions on Services Computing, 5(2):192-206, 2of2.","DOI":"10.1109\/TSC.2011.10"},{"key":"6_CR37","unstructured":"K. Havelund. Runtime verifieation of C programs. In Proc. of the 1st TestCom\/FATES conference, volume\u00a05047 of LNCS, 'Ibkyo, Japan, 2008. Springer."},{"key":"6_CR38","unstructured":"K. Havelund. Data automata in Scala. In M. Leucker and J. Wang, editors, 8th International Symposium on Theoretiool Aspects of Software Engineering, TASE 2of.1\" Changsha, China, September 1-3. Proceedings. IEEE Computer Society Press, 2of4."},{"key":"6_CR39","unstructured":"K. Havelund. Monitoring with data automata. In T. Margaria and B. Steffen, editors, 6th International Symposium On Levemging Applications of Formal Methods, Verijication and Validation. Track: Statistical Model Ghecking, Past Present and Puture (organized by Kim Larsen and Axel Legay), Corfu, Greece, October 8-11. Proceedings, volume\u00a08803 of LNCS, pages 254-273. Springer, 2of4."},{"key":"6_CR40","unstructured":"K. Havelund. Rule-based runtime verification revisited. Software Tools for Tech nology Transfer (STTT), April 2of4. Published online."},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"K. Havelund and A. Goldberg. Verify your runs. In Verijied Software: Theories, Tools, Experiments, VSTTE 2005, pages 374-383, 2008.","DOI":"10.1007\/978-3-540-69149-5_40"},{"issue":"2","key":"6_CR42","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K. Havelund and G.","year":"2004","unstructured":"K. Havelund and G. R.o\u00a7u. Eflieient monitoring of safety properties. Software Tools for Technology Transfer, 6(2):158\u2013173, 2004.","journal-title":"Software Tools for Technology Transfer"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"K. Havelund and G. Rosu. Monitoring programs using rewriting. In 16th ASE conferenee, San Diego, CA , USA, pages 135-143, 20of.","DOI":"10.1109\/ASE.2001.989799"},{"key":"6_CR44","unstructured":"G. J. Holzmann. The Spin Model Checker \u2013 Primer and Re\/erence Manual. Addison-Wesley, 2004."},{"key":"6_CR45","unstructured":"Jess website: http:\/\/www.jessrules.comfjess."},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. G. Griswold. An overview of AspectJ. In J. L. Knudsen, editor, Proc. of the 15th European Con\/erence on Object-Oriented Programming, volume\u00a02072 of LNCS, pages 327- 353. Springer, 20of.","DOI":"10.1007\/3-540-45337-7_18"},{"key":"6_CR47","unstructured":"C. Lee, D. Jin, P. O. Meredith, and G. Ro\u00a7u. Towards categorizing and formalizing the JDK API. Tecbnical Report http:\/\/hdl.handle.net\/2142\/30006, Department of Computer Science, University of Illinois at Urbana-Champaign, March 2of2."},{"key":"6_CR48","unstructured":"I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan. Runtime assurance based on formal specifications. In PDPTA, pages 279\u2013287. CSREA Press, 1999."},{"key":"6_CR49","doi-asserted-by":"crossref","unstructured":"M. Leucker and C. Schallhart. Abrief account of runtime verification. Journal of Logic and Algebraic Programming, 78(5):293-303, may \/june 2008.","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"6_CR50","unstructured":"D. Luckham, editor. The Power of Events: An Introduction to Gomplex Event Processing in Distributed Enterprise Systems. Addison-Wesley, 2002."},{"key":"6_CR51","doi-asserted-by":"crossref","unstructured":"P. Meredith, D. Jin, D. Griffith, F. Chen, and G. Ro\u00a7u. An overview of the MOP runtime verification framework. Software Tools \/or Technology Trans\/er (STTT), 14(3):249-289, 2of2.","DOI":"10.1007\/s10009-011-0198-6"},{"key":"6_CR52","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporallogic of programs. In 18th Annual Symposium on Foun dations of Computer Science, pages 46\u201357. IEEE Computer Society, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"6_CR53","unstructured":"G. Reger. Automata Based Monitoring and Mining of Execution 'lTaces . PhD thesis, University of Manchester, 2014."},{"key":"6_CR54","unstructured":"G. Reger, H. C. Cruz, and D. Rydeheard. MARQ: monitoring at runtime with QEA. In Proceedings of the 21st International Con\/erence on Tools and Algorithms \/or the Constmction and Analysis of Systems (TACAS'15), 2o15."},{"key":"6_CR55","unstructured":"Rooscaloo website: http:\/\/code.google.com\/p\/rooscaloo."},{"key":"6_CR56","doi-asserted-by":"crossref","unstructured":"M. Smith, G. Holzmann, and K. Ettessami. Events and constraints: a graphical editor for capturing logic properties of programs. In 5th [nt Sym . on Requirements Engineering, Toronto, Canada , volume 55(2), pages 14-22. 2001.","DOI":"10.1109\/ISRE.2001.948539"},{"key":"6_CR57","doi-asserted-by":"crossref","unstructured":"V. Stolz. Temporal assertians with parameterized propositions. In Proc. of the 7th Int. Workshop on Runtime Verijication (RV'07), volume\u00a04839 of LNCS, pages 176-187, Vancouver, Canada, 2007. Springer.","DOI":"10.1007\/978-3-540-77395-5_15"},{"key":"6_CR58","doi-asserted-by":"crossref","unstructured":"V. Stolz and E. Bodden. Temporal assertians using AspectJ. In Proc. of the 5 th Int. Workshop on Runtime Verijication (RV'05), volume 144(4) of ENTCS, pages 109\u2013124. Elsevier, 2006.","DOI":"10.1016\/j.entcs.2006.02.007"},{"key":"6_CR59","doi-asserted-by":"crossref","unstructured":"V. Stolz and F. Huch. Runtime verification of concurrent Haskell programs. In Proc. of the 4th Int. Workshop on Runtime Verijication (RV'04), volume\u00a0113 of ENTCS, pages 2of-216. Elsevier, 2005.","DOI":"10.1016\/j.entcs.2004.01.026"},{"key":"6_CR60","doi-asserted-by":"crossref","unstructured":"M. Vardi. From Church and Prior to PSL. In O. Grumberg and H. Veith, editors, 25 Years of Model Checking , volume\u00a05000 of Lecture Notes in Computer Science , pages 150\u2013171. Springer Berlin Heidelberg, 2008.","DOI":"10.1007\/978-3-540-69850-0_10"}],"container-title":["Formal Modeling and Verification of Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-658-09994-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T10:37:00Z","timestamp":1748428620000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-658-09994-7_6"}},"subtitle":["Quantified Event Automata versus Rule Systems"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783658099930","9783658099947"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-658-09994-7_6","relation":{},"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"6 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}