{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T05:20:54Z","timestamp":1725772854531},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642546235"},{"type":"electronic","value":"9783642546242"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-642-54624-2_28","type":"book-chapter","created":{"date-parts":[[2014,2,28]],"date-time":"2014-02-28T17:42:59Z","timestamp":1393609379000},"page":"560-577","source":"Crossref","is-referenced-by-count":4,"title":["Verifying the Design of Dynamic Software Updating in the OTS\/CafeOBJ Method"],"prefix":"10.1007","author":[{"given":"Min","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"publisher","first-page":"1049","DOI":"10.1145\/1108970.1108971","volume":"27","author":"M. Hicks","year":"2005","unstructured":"Hicks, M., Nettles, S.: Dynamic software updating. ACM TOPLAS\u00a027, 1049\u20131096 (2005)","journal-title":"ACM TOPLAS"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Duggan, D.: Type-based hot swapping of running modules. In: Functional Programming, vol.\u00a036, pp. 62\u201373. ACM (2001)","DOI":"10.1145\/507669.507645"},{"key":"28_CR3","first-page":"183","volume":"40","author":"G. Stoyle","year":"2005","unstructured":"Stoyle, G., Hicks, M., Bierman, G., et al.: Mutatis mutandis: safe and predictable dynamic software updating. ACM TOPLAS\u00a040, 183\u2013194 (2005)","journal-title":"ACM TOPLAS"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Neamtiu, I., Hicks, M., Foster, J., et al.: Contextual effects for version-consistent dynamic software updating and safe concurrent programming. In: POPL, vol.\u00a043, pp. 37\u201349. ACM (2008)","DOI":"10.1145\/1328897.1328447"},{"issue":"2","key":"28_CR5","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1109\/32.485222","volume":"22","author":"D. Gupta","year":"1996","unstructured":"Gupta, D., Jalote, P., Barua, G.: A formal framework for on-line software version change. IEEE Transactions on Software Engineering\u00a022(2), 120\u2013131 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-27705-4_22","volume-title":"Verified Software: Theories, Tools, Experiments","author":"C.M. Hayden","year":"2012","unstructured":"Hayden, C.M., Magill, S., Hicks, M., Foster, N., Foster, J.S.: Specifying and verifying the correctness of dynamic software updates. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 278\u2013293. Springer, Heidelberg (2012)"},{"key":"28_CR7","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/j.entcs.2013.02.013","volume":"294","author":"M. Zhang","year":"2013","unstructured":"Zhang, M., Ogata, K., Futatsugi, K.: Formalization and verification of behavioral correctness of dynamic software updates. Electr. Notes Theor. Comput. Sci.\u00a0294, 12\u201323 (2013)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-540-69149-5_30","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K. Futatsugi","year":"2008","unstructured":"Futatsugi, K., Goguen, J.A., Ogata, K.: Verifying design with proof scores. In: Meyer, B., Woodcock, J. (eds.) Verified Software. LNCS, vol.\u00a04171, pp. 277\u2013290. Springer, Heidelberg (2008)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-39958-2_12","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Proof scores in the OTS\/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 170\u2013184. Springer, Heidelberg (2003)"},{"key":"28_CR10","first-page":"771","volume":"19","author":"K. Ogata","year":"2013","unstructured":"Ogata, K., Futatsugi, K.: Compositionally writing proof scores of invariants in the OTS\/CafeOBJ method. J. UCS\u00a019, 771\u2013804 (2013)","journal-title":"J. UCS"},{"key":"28_CR11","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.entcs.2008.02.018","volume":"201","author":"K. Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the OTS\/CafeOBJ method. Electr. Notes Theor. Comput. Sci.\u00a0201, 127\u2013154 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"28_CR12","doi-asserted-by":"publisher","first-page":"974","DOI":"10.1587\/transinf.E93.D.974","volume":"93-D","author":"W. Kong","year":"2010","unstructured":"Kong, W., Ogata, K., Futatsugi, K.: Towards reliable E-Government systems with the OTS\/CafeOBJ method. IEICE Transactions\u00a093-D, 974\u2013984 (2010)","journal-title":"IEICE Transactions"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-36532-X_25","volume-title":"Software Security \u2013 Theories and Systems","author":"K. Hasebe","year":"2003","unstructured":"Hasebe, K., Okada, M.: Formal analysis of the ikp electronic payment protocols. In: Okada, M., Babu, C. S., Scedrov, A., Tokuda, H. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 441\u2013460. Springer, Heidelberg (2003)"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-36384-X_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Ogata","year":"2002","unstructured":"Ogata, K., Futatsugi, K.: Formal verification of the horn-preneel micropayment protocol. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 238\u2013252. Springer, Heidelberg (2002)"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-88194-0_13","volume-title":"Formal Methods and Software Engineering","author":"K. Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Formal analysis of the bakery protocol with consideration of nonatomic reads and writes. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 187\u2013207. Springer, Heidelberg (2008)"},{"key":"28_CR16","first-page":"949","volume":"23","author":"D. Gupta","year":"1993","unstructured":"Gupta, D., Jalote, P.: On-line software version change using state transfer between processes. Software: Practice and Experience\u00a023, 949\u2013964 (1993)","journal-title":"Software: Practice and Experience"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Neamtiu, I., Hicks, M.W., Stoyle, G., et al.: Practical dynamic software updating for c. In: PLDI, ACM SIGPLAN, pp. 72\u201383 (2006)","DOI":"10.1145\/1133255.1133991"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Chen, H., Yu, J., Hang, C., et al.: Dynamic software updating using a relaxed consistency model. IEEE Transactions on Software Engineering (99), 679\u2013694 (2011)","DOI":"10.1109\/TSE.2010.79"},{"key":"28_CR19","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1109\/52.199735","volume":"10","author":"M. Segal","year":"1993","unstructured":"Segal, M., Frieder, O.: On-the-fly program modification: Systems for dynamic updating. IEEE Software\u00a010, 53\u201365 (1993)","journal-title":"IEEE Software"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Hayden, C.M., Smith, E.K., Denchev, M., Hicks, M., Foster, J.S.: Kitsune: Efficient, general-purpose dynamic software updating for c. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, pp. 249\u2013264. ACM (2012)","DOI":"10.1145\/2384616.2384635"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ report: The language. In: Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, vol. 6 (1998)","DOI":"10.1142\/3831"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/11780274_31","volume-title":"Algebra, Meaning, and Computation","author":"K. Ogata","year":"2006","unstructured":"Ogata, K., Futatsugi, K.: Some tips on writing proof scores in the OTS\/CafeOBJ method. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Goguen Festschrift. LNCS, vol.\u00a04060, pp. 596\u2013615. Springer, Heidelberg (2006)"},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"28_CR24","doi-asserted-by":"publisher","first-page":"976","DOI":"10.1587\/transinf.E94.D.976","volume":"94-D","author":"M. Zhang","year":"2011","unstructured":"Zhang, M., Ogata, K., Nakamura, M.: Translation of state machines from equational theories into rewrite theories with tool support. IEICE Transactions on Information and Systems\u00a094-D, 976\u2013988 (2011)","journal-title":"IEICE Transactions on Information and Systems"},{"key":"28_CR25","doi-asserted-by":"publisher","first-page":"1492","DOI":"10.1093\/ietisy\/e91-d.5.1492","volume":"91-D","author":"M. Nakamura","year":"2008","unstructured":"Nakamura, M., Kong, W., et al.: A specification translation from behavioral specifications to rewrite specifications. IEICE Transactions\u00a091-D, 1492\u20131503 (2008)","journal-title":"IEICE Transactions"},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11901433_7","volume-title":"Formal Methods and Software Engineering","author":"K. Ogata","year":"2006","unstructured":"Ogata, K., Nakano, M., Kong, W., Futatsugi, K.: Induction-guided falsification. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 114\u2013131. Springer, Heidelberg (2006)"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"Zhang, J., Cheng, B.H.C.: Model-based development of dynamically adaptive software. In: ICSE, pp. 371\u2013380. IEEE (2006)","DOI":"10.1145\/1134285.1134337"}],"container-title":["Lecture Notes in Computer Science","Specification, Algebra, and Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54624-2_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T06:06:51Z","timestamp":1558850811000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54624-2_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642546235","9783642546242"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54624-2_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}