{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T08:55:05Z","timestamp":1780563305044,"version":"3.54.1"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030378721","type":"print"},{"value":"9783030378738","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[[2020]]},"DOI":"10.1007\/978-3-030-37873-8_14","type":"book-chapter","created":{"date-parts":[[2020,1,2]],"date-time":"2020-01-02T20:03:00Z","timestamp":1577995380000},"page":"320-349","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Framework for Flexible Program Evolution and Verification of Distributed Systems"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Owe","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Elahe","family":"Fazeldehkordi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jia-Chun","family":"Lin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,1,3]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11785477_26","volume-title":"ECOOP 2006 \u2013 Object-Oriented Programming","author":"S Ajmani","year":"2006","unstructured":"Ajmani, S., Liskov, B., Shrira, L.: Modular software upgrades for distributed systems. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 452\u2013476. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11785477_26"},{"issue":"2\u20133","key":"14_CR2","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/j.scico.2007.04.002","volume":"67","author":"R Banach","year":"2007","unstructured":"Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and theoretical underpinnings of retrenchment. Sci. Comput. Program. 67(2\u20133), 301\u2013329 (2007)","journal-title":"Sci. Comput. Program."},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/11813040_33","volume-title":"FM 2006: Formal Methods","author":"F Bannwart","year":"2006","unstructured":"Bannwart, F., M\u00fcller, P.: Changing programs correctly: refactoring with specifications. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 492\u2013507. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11813040_33"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-46508-1_8","volume":"1","author":"R Bubel","year":"2016","unstructured":"Bubel, R., et al.: Proof repositories for compositional verification of evolving software systems - managing change when proving software correct. Trans. Found. Mastering Change 1, 130\u2013156 (2016)","journal-title":"Trans. Found. Mastering Change"},{"key":"14_CR5","unstructured":"Clavel, M., et al.: Maude manual (version 2.4) (2008)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Din, C.C., Johnsen, E.B., Owe, O., Yu, I.C.: A modular reasoning system using uninterpreted predicates for code reuse. J. Logical Algebraic Methods Program. 95, 82\u2013102 (2018)","DOI":"10.1016\/j.jlamp.2017.11.004"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Din, C.C., Owe, O.: A sound and complete reasoning system for asynchronous communication with shared futures. J. Logical Algeb. Methods Program. 83(5\u20136), 360\u2013383 (2014)","DOI":"10.1016\/j.jlamp.2014.03.003"},{"issue":"7","key":"14_CR8","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1016\/j.jlap.2010.07.008","volume":"79","author":"J Dovland","year":"2010","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. J. Logic Algebraic Program. 79(7), 578\u2013607 (2010)","journal-title":"J. Logic Algebraic Program."},{"issue":"10","key":"14_CR9","doi-asserted-by":"publisher","first-page":"915","DOI":"10.1016\/j.scico.2010.09.006","volume":"76","author":"J Dovland","year":"2011","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Incremental reasoning with lazy behavioral subtyping for multiple inheritance. Sci. Comput. Program. 76(10), 915\u2013941 (2011)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"14_CR10","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.jlamp.2014.09.001","volume":"84","author":"J Dovland","year":"2015","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Yu, I.C.: A proof system for adaptable class hierarchies. J. Logical Algebraic Methods Program. 84(1), 37\u201353 (2015)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-642-34026-0_19","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"J Dovland","year":"2012","unstructured":"Dovland, J., Johnsen, E.B., Yu, I.C.: Tracking behavioral constraints during object-oriented software evolution. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 253\u2013268. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-34026-0_19"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Fu, Z., Smith, G.: Towards more flexible development of Z specifications. In: 2nd IFIP\/IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 281\u2013288, June 2008","DOI":"10.1109\/TASE.2008.20"},{"issue":"1","key":"14_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11704-010-0112-5","volume":"5","author":"Z Fu","year":"2011","unstructured":"Fu, Z., Smith, G.: Property transformation under specification change. Front. Comput. Sci. China 5(1), 1\u201313 (2011)","journal-title":"Front. Comput. Sci. China"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-38574-2_21","volume-title":"Automated Deduction \u2013 CADE-24","author":"R H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 300\u2013314. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38574-2_21"},{"issue":"1","key":"14_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10270-006-0011-2","volume":"6","author":"EB Johnsen","year":"2007","unstructured":"Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Softw. Syst. Model. 6(1), 35\u201358 (2007)","journal-title":"Softw. Syst. Model."},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/11494881_2","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"EB Johnsen","year":"2005","unstructured":"Johnsen, E.B., Owe, O., Simplot-Ryl, I.: A dynamic class construct for asynchronous concurrent objects. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 15\u201330. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11494881_2"},{"issue":"1\u20132","key":"14_CR17","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.tcs.2006.07.031","volume":"365","author":"EB Johnsen","year":"2006","unstructured":"Johnsen, E.B., Owe, O., Yu, I.C.: Creol: a type-safe object-oriented model for distributed concurrent systems. Theoret. Comput. Sci. 365(1\u20132), 23\u201366 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"14_CR18","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1016\/j.jlamp.2018.11.008","volume":"103","author":"F Karami","year":"2019","unstructured":"Karami, F., Owe, O., Ramezanifarkhani, T.: An evaluation of interaction paradigms for active objects. J. Logical Algebraic Methods Program. 103, 154\u2013183 (2019)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"14_CR19","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Owe, O.: Verifiable programming of object-oriented and distributed systems. In: Petre, L., Sekerinski, E. (eds.) From Action System to Distributed Systems: The Refinement Approach, pp. 61\u201380. Taylor&Francis (2015)","DOI":"10.1201\/b20053-8"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-319-33693-0_14","volume-title":"Integrated Formal Methods","author":"O Owe","year":"2016","unstructured":"Owe, O.: Reasoning about inheritance and unrestricted reuse in object-oriented concurrent systems. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 210\u2013225. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33693-0_14"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Owe, O., Lin, J.-C., Fazeldehkordi, E.: A flexible framework for program evolution and verification. In: 7th International Conference on Model-Driven Engineering and Software Development (Modelsward 2019), February 2019","DOI":"10.5220\/0007690301770189"},{"key":"14_CR23","unstructured":"Owe, O., Ryl, I.: On combining object orientation, openness and reliability. In: Proceedings of the Norwegian Informatics Conference (NIK 1999), Tapir, pp. 187\u2013198, November 1999"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-57529-4_61","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"W Reif","year":"1993","unstructured":"Reif, W., Stenzel, K.: Reuse of proofs in software verification. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 284\u2013293. Springer, Heidelberg (1993). \nhttps:\/\/doi.org\/10.1007\/3-540-57529-4_61"},{"issue":"5","key":"14_CR25","first-page":"535","volume":"25","author":"H Seifzadeh","year":"2013","unstructured":"Seifzadeh, H., Abolhassani, H., Moshkenani, M.S.: A survey of dynamic software updating. J. Softw.: Evol. Process 25(5), 535\u2013568 (2013)","journal-title":"J. Softw.: Evol. Process"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Ulewicz, S., et al.: A verification-supported evolution approach to assist software application engineers in industrial factory automation. In: 2016 IEEE International Symposium on Assembly and Manufacturing (ISAM), pp. 19\u201325, August 2016","DOI":"10.1109\/ISAM.2016.7750714"},{"issue":"01","key":"14_CR27","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1142\/S0218194095000034","volume":"05","author":"MP Ward","year":"1995","unstructured":"Ward, M.P., Bennett, K.H.: Formal methods to aid the evolution of software. Int. J. Softw. Eng. Knowl. Eng. 05(01), 25\u201347 (1995)","journal-title":"Int. J. Softw. Eng. Knowl. Eng."}],"container-title":["Communications in Computer and Information Science","Model-Driven Engineering and Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-37873-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,3]],"date-time":"2020-01-03T01:12:43Z","timestamp":1578013963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-37873-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030378721","9783030378738"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-37873-8_14","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"value":"1865-0929","type":"print"},{"value":"1865-0937","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"3 January 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MODELSWARD","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Model-Driven Engineering and Software Development","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 February 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 February 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"modelsward2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.modelsward.org\/?y=2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"PRIMORIS","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}