{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T09:05:49Z","timestamp":1726045549140},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030315139"},{"type":"electronic","value":"9783030315146"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31514-6_16","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T19:03:06Z","timestamp":1569178986000},"page":"276-293","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Runtime Verification of Parametric Properties Using SMEDL"],"prefix":"10.1007","author":[{"given":"Teng","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramneet","family":"Kaur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Allan, C., et al.: Adding trace matching with free variables to AspectJ. In: ACM SIGPLAN Notices, vol. 40, pp. 345\u2013364. ACM (2005)","DOI":"10.1145\/1103845.1094839"},{"key":"16_CR2","unstructured":"Azzopardi, S., Colombo, C., Ebejer, J.P., Mallia, E., Pace, G.J.: Runtime verification using VALOUR (2017)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-11164-3_3","volume-title":"Runtime Verification","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Two generalisations of Ro\u015fu and Chen\u2019s trace slicing Algorithm A. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 15\u201330. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-11164-3_3"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-32759-9_9","volume-title":"FM 2012: Formal Methods","author":"H Barringer","year":"2012","unstructured":"Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68\u201384. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-32759-9_9"},{"key":"16_CR5","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24622-0_5"},{"issue":"11","key":"16_CR6","doi-asserted-by":"publisher","first-page":"365","DOI":"10.2514\/1.49356","volume":"7","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.: Formal analysis of log files. J. Aerosp. Comput. Inf. Commun. 7(11), 365\u2013390 (2010)","journal-title":"J. Aerosp. Comput. Inf. Commun."},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-21437-0_7","volume-title":"FM 2011: Formal Methods","author":"H Barringer","year":"2011","unstructured":"Barringer, H., Havelund, K.: TraceContract: a Scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57\u201372. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-21437-0_7"},{"issue":"3","key":"16_CR8","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput. 20(3), 675\u2013706 (2010)","journal-title":"J. Log. Comput."},{"issue":"2","key":"16_CR9","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/2699444","volume":"62","author":"D Basin","year":"2015","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S., Z\u0103linescu, E.: Monitoring metric first-order temporal properties. J. ACM (JACM) 62(2), 15 (2015)","journal-title":"J. ACM (JACM)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-40787-1_4","volume-title":"Runtime Verification","author":"A Bauer","year":"2013","unstructured":"Bauer, A., K\u00fcster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59\u201375. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-40787-1_4"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-00768-2_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Chen","year":"2009","unstructured":"Chen, F., Ro\u015fu, G.: Parametric trace slicing and monitoring. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 246\u2013261. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-00768-2_23"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-662-49674-9_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z Chen","year":"2016","unstructured":"Chen, Z., Wang, Z., Zhu, Y., Xi, H., Yang, Z.: Parametric runtime verification of C programs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 299\u2013315. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_17"},{"key":"16_CR13","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-33826-7_15"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-03240-0_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"C Colombo","year":"2009","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 135\u2013149. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-03240-0_13"},{"key":"16_CR15","unstructured":"d\u2019Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning, TIME 2005, pp. 166\u2013174. IEEE (2005)"},{"issue":"2","key":"16_CR16","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.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. 18(2), 205\u2013225 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-46982-9_10","volume-title":"Runtime Verification","author":"P Faymonville","year":"2016","unstructured":"Faymonville, P., Finkbeiner, B., Schirmer, S., Torfah, H.: A stream-based specification language for network monitoring. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 152\u2013168. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46982-9_10"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-89247-2_1","volume-title":"Runtime Verification","author":"J Goubault-Larrecq","year":"2008","unstructured":"Goubault-Larrecq, J., Olivain, J.: A smell of Orchids. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 1\u201320. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-89247-2_1"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-36742-7_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Grigore","year":"2013","unstructured":"Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 260\u2013276. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-36742-7_19"},{"issue":"2","key":"16_CR20","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/TSC.2011.10","volume":"5","author":"S Hall\u00e9","year":"2012","unstructured":"Hall\u00e9, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192\u2013206 (2012)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-662-45231-8_18","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications","author":"K Havelund","year":"2014","unstructured":"Havelund, K.: Monitoring with data automata. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 254\u2013273. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-662-45231-8_18"},{"issue":"2","key":"16_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.: Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Transf. 17(2), 143\u2013170 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"16_CR23","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329\u2013363 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"ECOOP 2001 \u2014 Object-Oriented Programming","author":"G Kiczales","year":"2001","unstructured":"Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327\u2013354. Springer, Heidelberg (2001). \n                      https:\/\/doi.org\/10.1007\/3-540-45337-7_18"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-11164-3_24","volume-title":"Runtime Verification","author":"Q Luo","year":"2014","unstructured":"Luo, Q., et al.: RV-Monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 285\u2013300. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-11164-3_24"},{"issue":"3","key":"16_CR26","doi-asserted-by":"publisher","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., Ro\u015fu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. 14(3), 249\u2013289 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"16_CR27","unstructured":"Reger, G.: Automata based monitoring and mining of execution traces. Ph.D. thesis, University of Manchester (2014)"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-319-23820-3_14","volume-title":"Runtime Verification","author":"G Reger","year":"2015","unstructured":"Reger, G., Rydeheard, D.: From first-order temporal logic to parametric trace slicing. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 216\u2013232. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-23820-3_14"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-030-03769-7_19","volume-title":"Runtime Verification","author":"G Reger","year":"2018","unstructured":"Reger, G., Rydeheard, D.: From parametric trace slicing to rule systems. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 334\u2013352. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-03769-7_19"},{"issue":"4","key":"16_CR30","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.entcs.2006.02.007","volume":"144","author":"V Stolz","year":"2006","unstructured":"Stolz, V., Bodden, E.: Temporal assertions using AspectJ. Electron. Notes Theor. Comput. Sci. 144(4), 109\u2013124 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"16_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-46982-9_24","volume-title":"Runtime Verification","author":"Y Yamagata","year":"2016","unstructured":"Yamagata, Y., et al.: Runtime monitoring for concurrent systems. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 386\u2013403. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46982-9_24"},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-030-03427-6_6","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"T Zhang","year":"2018","unstructured":"Zhang, T., Eakman, G., Lee, I., Sokolsky, O.: Flexible monitor deployment for runtime verification of large scale software. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 42\u201350. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-03427-6_6"},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-319-46982-9_32","volume-title":"Runtime Verification","author":"T Zhang","year":"2016","unstructured":"Zhang, T., Gebhard, P., Sokolsky, O.: SMEDL: combining synchronous and asynchronous monitoring. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 482\u2013490. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46982-9_32"},{"key":"16_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-99933-3_3","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"T Zhang","year":"2018","unstructured":"Zhang, T., et al.: Correct-by-construction implementation of runtime monitors using stepwise refinement. In: Feng, X., M\u00fcller-Olm, M., Yang, Z. (eds.) SETTA 2018. LNCS, vol. 10998, pp. 31\u201349. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-99933-3_3"}],"container-title":["Lecture Notes in Computer Science","From Reactive Systems to Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31514-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T19:27:32Z","timestamp":1569180452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31514-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030315139","9783030315146"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31514-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}