{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T11:03:26Z","timestamp":1781175806466,"version":"3.54.1"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319675305","type":"print"},{"value":"9783319675312","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67531-2_2","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T05:33:37Z","timestamp":1504589617000},"page":"8-29","source":"Crossref","is-referenced-by-count":28,"title":["A Foundation for Runtime Monitoring"],"prefix":"10.1007","author":[{"given":"Adrian","family":"Francalanza","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luca","family":"Aceto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antonis","family":"Achilleos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Duncan Paul","family":"Attard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ian","family":"Cassar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dario","family":"Della Monica","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anna","family":"Ing\u00f3lfsd\u00f3ttir","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-60134-2_1","volume-title":"Implementation and Application of Automata","author":"L Aceto","year":"2017","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Kjartansson, S.\u00d6.: On the complexity of determinizing monitors. In: Carayol, A., Nicaud, C. (eds.) CIAA 2017. LNCS, vol. 10329, pp. 1\u201313. Springer, Cham (2017). doi: 10.1007\/978-3-319-60134-2_1"},{"key":"2_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive Systems: Modelling, Specification and Verification","author":"L Aceto","year":"2007","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-19249-9_8","volume-title":"FM 2015: Formal Methods","author":"W Ahrendt","year":"2015","unstructured":"Ahrendt, W., Chimento, J.M., Pace, G.J., Schneider, G.: A specification language for static and runtime verification of data and control properties. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 108\u2013125. Springer, Cham (2015). doi: 10.1007\/978-3-319-19249-9_8"},{"issue":"1\u20132","key":"2_CR4","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.scico.2008.09.004","volume":"74","author":"I Aktug","year":"2008","unstructured":"Aktug, I., Naliuka, K.: ConSpec - a formal language for policy specification. Sci. Comput. Program. 74(1\u20132), 2\u201312 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"2\u20133","key":"2_CR5","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/j.tcs.2004.11.007","volume":"336","author":"C Artho","year":"2005","unstructured":"Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M.R., Pasareanu, C.S., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test case generation and runtime verification. Theor. Comput. Sci. 336(2\u20133), 209\u2013234 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-319-46982-9_31","volume-title":"Runtime Verification","author":"DP Attard","year":"2016","unstructured":"Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 473\u2013481. Springer, Cham (2016). doi: 10.1007\/978-3-319-46982-9_31"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Attard, D.P., Francalanza, A.: Trace partitioning and local monitoring for asynchronous components. In: SEFM, LNCS (2017, to appear)","DOI":"10.1007\/978-3-319-66197-1_14"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-319-41591-8_23","volume-title":"Software Engineering and Formal Methods","author":"S Azzopardi","year":"2016","unstructured":"Azzopardi, S., Colombo, C., Pace, G.J., Vella, B.: Compliance checking in the open payments ecosystem. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 337\u2013343. Springer, Cham (2016). doi: 10.1007\/978-3-319-41591-8_23"},{"key":"2_CR9","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, New York (2008)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44\u201357. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24622-0_5"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-35632-2_17","volume-title":"Runtime Verification","author":"D Basin","year":"2013","unstructured":"Basin, D., Klaedtke, F., Marinovic, S., Z\u0103linescu, E.: Monitoring compliance policies over incomplete and disagreeing logs. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 151\u2013167. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35632-2_17"},{"issue":"2\u20133","key":"2_CR12","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/B:FORM.0000040027.28662.a4","volume":"25","author":"GP Brat","year":"2004","unstructured":"Brat, G.P., Drusinsky, D., Giannakopoulou, D., Goldberg, A., Havelund, K., Lowry, M.R., Pasareanu, C.S., Venet, A., Visser, W., Washington, R.: Experimental evaluation of verification and validation tools on martian rover software. Formal Methods Syst. Des. 25(2\u20133), 167\u2013198 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-23820-3_3","volume-title":"Runtime Verification","author":"I Cassar","year":"2015","unstructured":"Cassar, I., Francalanza, A.: Runtime adaptation for actor systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 38\u201354. Springer, Cham (2015). doi: 10.1007\/978-3-319-23820-3_3"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-33693-0_12","volume-title":"Integrated Formal Methods","author":"I Cassar","year":"2016","unstructured":"Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 176\u2013192. Springer, Cham (2016). doi: 10.1007\/978-3-319-33693-0_12"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Cassar, I., Francalanza, A., Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: eAOP - an aspect oriented programming framework for erlang. In: Erlang Workshop (2017, to appear)","DOI":"10.1145\/3123569.3123570"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Chen, F., Rosu, G.: MOP: an efficient and generic runtime verification framework. In: OOPSLA, pp. 569\u2013588 (2007)","DOI":"10.1145\/1297027.1297069"},{"key":"2_CR17","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-33826-7_15","volume-title":"Software Engineering and Formal Methods","author":"C Colombo","year":"2012","unstructured":"Colombo, C., Francalanza, A., Mizzi, R., Pace, G.J.: polyLarva: runtime verification with configurable resource-aware monitoring boundaries. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 218\u2013232. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33826-7_15"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: TIME, pp. 166\u2013174 (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-319-19249-9_10","volume-title":"FM 2015: Formal Methods","author":"S Debois","year":"2015","unstructured":"Debois, S., Hildebrandt, T., Slaats, T.: Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 143\u2013160. Springer, Cham (2015). doi: 10.1007\/978-3-319-19249-9_10"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-38088-4_34","volume-title":"NASA Formal Methods","author":"N Decker","year":"2013","unstructured":"Decker, N., Leucker, M., Thoma, D.: jUnitRV\u2013adding runtime verification to jUnit. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 459\u2013464. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38088-4_34"},{"key":"2_CR22","unstructured":"Monica, D.D., Francalanza, A.: Towards a hybrid approach to software verification. In: NWPT, number SCS16001 in RUTR, pp. 51\u201354 (2015)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-49630-5_9","volume-title":"Foundations of Software Science and Computation Structures","author":"A Francalanza","year":"2016","unstructured":"Francalanza, A.: A theory of monitors. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 145\u2013161. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49630-5_9"},{"key":"2_CR24","unstructured":"Francalanza, A.: Consistently-detecting monitors. In: CONCUR. Dagstuhl Publishing (LIPICS) (2017)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-23820-3_5","volume-title":"Runtime Verification","author":"A Francalanza","year":"2015","unstructured":"Francalanza, A., Aceto, L., Ingolfsdottir, A.: On verifying hennessy-milner logic with recursion at runtime. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 71\u201386. Springer, Cham (2015). doi: 10.1007\/978-3-319-23820-3_5"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Francalanza, A., Aceto, L., Ingolfsdottir, A.: Monitorability for the hennessy-milner logic with recursion. Formal Methods Syst. Des., 1\u201330 (2017)","DOI":"10.1007\/s10703-017-0273-z"},{"issue":"3","key":"2_CR27","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/s10703-014-0217-9","volume":"46","author":"A Francalanza","year":"2015","unstructured":"Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Methods Syst. Des. 46(3), 226\u2013261 (2015)","journal-title":"Formal Methods Syst. Des."},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-23820-3_7","volume-title":"Runtime Verification","author":"A Kane","year":"2015","unstructured":"Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 102\u2013117. Springer, Cham (2015). doi: 10.1007\/978-3-319-23820-3_7"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-23820-3_8","volume-title":"Runtime Verification","author":"A Kassem","year":"2015","unstructured":"Kassem, A., Falcone, Y., Lafourcade, P.: Monitoring electronic exams. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 118\u2013135. Springer, Cham (2015). doi: 10.1007\/978-3-319-23820-3_8"},{"issue":"2","key":"2_CR30","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M Kim","year":"2004","unstructured":"Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for Java programs. Formal Methods Syst. Des. 24(2), 129\u2013155 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"2_CR31","unstructured":"Klamka, J.: system characteristics: stability, controllability, observability. In: Control System, Robotics and Automation, EOLLS, vol. 7 (2009)"},{"key":"2_CR32","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\upmu $$ -calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"2&3","key":"2_CR33","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Proof systems for satisfiability in hennessy-milner logic with recursion. Theor. Comput. Sci. 72(2&3), 265\u2013288 (1990)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-45139-0_6","volume-title":"Model Checking Software","author":"F Lerda","year":"2001","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 80\u2013102. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45139-0_6"},{"issue":"5","key":"2_CR35","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293\u2013303 (2009)","journal-title":"J. Log. Algebr. Program."},{"issue":"1\u20132","key":"2_CR36","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1\u20132), 2\u201316 (2005)","journal-title":"Int. J. Inf. Secur."},{"issue":"3","key":"2_CR37","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2012","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14(3), 249\u2013289 (2012)","journal-title":"STTT"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: CC, pp. 98\u2013108 (2017)","DOI":"10.1145\/3033019.3033031"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/978-3-662-46681-0_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Reger","year":"2015","unstructured":"Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 596\u2013610. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_55"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-642-40787-1_23","volume-title":"Runtime Verification","author":"S Varvaressos","year":"2013","unstructured":"Varvaressos, S., Vaillancourt, D., Gaboury, S., Blondin Mass\u00e9, A., Hall\u00e9, S.: Runtime monitoring of temporal logic properties in a platform game. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 346\u2013351. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40787-1_23"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67531-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T00:19:05Z","timestamp":1570061945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67531-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675305","9783319675312"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67531-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}