{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:23:58Z","timestamp":1725989038363},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999326"},{"type":"electronic","value":"9783319999333"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99933-3_3","type":"book-chapter","created":{"date-parts":[[2018,8,25]],"date-time":"2018-08-25T12:33:39Z","timestamp":1535200419000},"page":"31-49","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Correct-by-Construction Implementation of Runtime Monitors Using Stepwise Refinement"],"prefix":"10.1007","author":[{"given":"Teng","family":"Zhang","sequence":"first","affiliation":[]},{"given":"John","family":"Wiegley","sequence":"additional","affiliation":[]},{"given":"Theophilos","family":"Giannakopoulos","sequence":"additional","affiliation":[]},{"given":"Gregory","family":"Eakman","sequence":"additional","affiliation":[]},{"given":"Cl\u00e9ment","family":"Pit-Claudel","sequence":"additional","affiliation":[]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,26]]},"reference":[{"issue":"3","key":"3_CR1","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10009-011-0218-6","volume":"14","author":"O Sokolsky","year":"2012","unstructured":"Sokolsky, O., Havelund, K., Lee, I.: Introduction to the special section on runtime verification. Softw. Tools Technol. Transf. 14(3), 243\u2013247 (2012)","journal-title":"Softw. Tools Technol. Transf."},{"key":"3_CR2","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). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_32"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Delaware, B., Pit-Claudel, C., Gross, J., Chlipala, A.: Fiat: Deductive synthesis of abstract data types in a proof assistant. In: ACM SIGPLAN Notices, vol. 50, pp. 689\u2013700. ACM (2015)","DOI":"10.1145\/2775051.2677006"},{"key":"3_CR4","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual"},{"key":"3_CR5","unstructured":"Chlipala, A., et al.: The end of history? using a proof assistant to replace language design with library design. In: SNAPL 2017: 2nd Summit on Advances in Programming Languages (2017)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Wiegley, J., Delaware, B.: Using Coq to write fast and correct Haskell. In: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, pp. 52\u201362. ACM (2017)","DOI":"10.1145\/3122955.3122962"},{"key":"3_CR7","unstructured":"Hoare, C., et al.: Data refinement refined (1985)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Cheng, K.T., Krishnakumar, A.S.: Automatic functional test generation using the extended finite state machine model. In: Proceedings of the 30th International Design Automation Conference, pp. 86\u201391. ACM (1993)","DOI":"10.1145\/157485.164585"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"MHA Newman","year":"1942","unstructured":"Newman, M.H.A.: On theories with a combinatorial definition of \u201cequivalence\u201d. Ann. Math. 43, 223\u2013243 (1942)","journal-title":"Ann. Math."},{"key":"3_CR10","unstructured":"Oniguruma contributors: Oniguruma. https:\/\/github.com\/kkos\/oniguruma . Accessed 27 Mar 2018"},{"key":"3_CR11","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). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_5"},{"key":"3_CR12","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\/1094811.1094839"},{"issue":"3","key":"3_CR13","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."},{"key":"3_CR14","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). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_23"},{"key":"3_CR15","unstructured":"Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Departmental Papers (CIS), pp. 294 (1999)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: 2001 Proceedings of 16th Annual International Conference on Automated Software Engineering. (ASE 2001), pp. 412\u2013416. IEEE (2001)","DOI":"10.1109\/ASE.2001.989841"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.01.025","volume":"113","author":"D Drusinsky","year":"2005","unstructured":"Drusinsky, D.: Semantics and runtime monitoring of tlcharts: statechart automata with temporal logic conditioned transitions. Electron. Notes Theor. Comput. Sci. 113, 3\u201321 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"3_CR18","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.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151\u2013197 (2005)","journal-title":"Autom. Softw. Eng."},{"key":"3_CR19","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). https:\/\/doi.org\/10.1007\/978-3-642-03240-0_13"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-540-68524-1_3","volume-title":"Testing of Software and Communicating Systems","author":"K Havelund","year":"2008","unstructured":"Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) FATES\/TestCom -2008. LNCS, vol. 5047, pp. 7\u201322. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68524-1_3"},{"issue":"3","key":"3_CR21","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":"3_CR22","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). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_24"},{"key":"3_CR23","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). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_17"},{"key":"3_CR24","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). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_55"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-45500-0_15","volume-title":"Theoretical Aspects of Computer Software","author":"C Paulin-Mohring","year":"2001","unstructured":"Paulin-Mohring, C.: Modelisation of timed automata in Coq. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 298\u2013315. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45500-0_15"},{"key":"3_CR26","unstructured":"Kamm\u00fcller, F., Helke, S.: Mechanical analysis of UML state machines and class diagrams. In: The Proceedings of Workshop on Precise Semantics for the UML. ECOOP2000. Citeseer (2000)"},{"issue":"3","key":"3_CR27","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"3_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Frana, R., Bodeveix, J.P., Filali, M., Rolland, J.F.: The AADL behaviour annex-experiments and roadmap. In: 2007 12th IEEE International Conference on Engineering Complex Computer Systems, 377\u2013382. IEEE (2007)","DOI":"10.1109\/ICECCS.2007.41"},{"key":"3_CR30","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.jss.2014.02.058","volume":"93","author":"Z Yang","year":"2014","unstructured":"Yang, Z., Hu, K., Ma, D., Bodeveix, J.P., Pi, L., Talpin, J.P.: From AADL to timed abstract state machines: a verified model transformation. J. Syst. Softw. 93, 42\u201368 (2014)","journal-title":"J. Syst. Softw."},{"key":"3_CR31","unstructured":"Ouimet, M., Lundqvist, K., Nolin, M.: The timed abstract state machine language: an executable specification language for reactive real-time systems. In: RTNS 2007, p. 15 (2007)"},{"issue":"3","key":"3_CR32","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/BF01933419","volume":"8","author":"EW Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: A constructive approach to the problem of program correctness. BIT Numer. Math. 8(3), 174\u2013186 (1968)","journal-title":"BIT Numer. Math."},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/3-540-60117-1_22","volume-title":"Mathematics of Program Construction","author":"YV Srinivas","year":"1995","unstructured":"Srinivas, Y.V., J\u00fcllig, R.: Specware: formal support for composing software. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 399\u2013422. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60117-1_22"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166\u2013182. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-03545-1_10","volume-title":"Certified Programs and Proofs","author":"C Cohen","year":"2013","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free!. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 147\u2013162. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_10"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-22102-1_17","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2015","unstructured":"Lammich, P.: Refinement to imperative\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253\u2013269. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_17"},{"key":"3_CR37","first-page":"1","volume":"77","author":"JR Abrial","year":"2007","unstructured":"Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to event-B. Fundam. Inform. 77, 1\u201328 (2007)","journal-title":"Fundam. Inform."}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99933-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T23:47:50Z","timestamp":1571788070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99933-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999326","9783319999333"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99933-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}