{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:36:03Z","timestamp":1763642163294,"version":"3.41.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T00:00:00Z","timestamp":1484006400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["17-12465S"],"award-info":[{"award-number":["17-12465S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"name":"EC within the H2020","award":["644579 (ESCUDO-CLOUD)"],"award-info":[{"award-number":["644579 (ESCUDO-CLOUD)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Auton. Adapt. Syst."],"published-print":{"date-parts":[[2017,2,3]]},"abstract":"<jats:p>Feedback control loops that monitor and adapt managed parts of a software system are considered crucial for realizing self-adaptation in software systems. The MAPE-K (Monitor-Analyze-Plan-Execute over a shared Knowledge) autonomic control loop is the most influential reference control model for self-adaptive systems. The design of complex distributed self-adaptive systems having decentralized adaptation control by multiple interacting MAPE components is among the major challenges. In particular, formal methods for designing and assuring the functional correctness of the decentralized adaptation logic are highly demanded.<\/jats:p>\n          <jats:p>\n            This article presents a framework for formal modeling and analyzing self-adaptive systems. We contribute with a formalism, called\n            <jats:italic>self-adaptive Abstract State Machines<\/jats:italic>\n            , that exploits the concept of multiagent Abstract State Machines to specify distributed and decentralized adaptation control in terms of MAPE-K control loops, also possible instances of MAPE patterns. We support validation and verification techniques for discovering unexpected interfering MAPE-K loops, and for assuring correctness of MAPE components interaction when performing adaptation.\n          <\/jats:p>","DOI":"10.1145\/3019598","type":"journal-article","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T15:41:17Z","timestamp":1484062877000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":53,"title":["Formal Design and Verification of Self-Adaptive Systems with Decentralized Control"],"prefix":"10.1145","volume":"11","author":[{"given":"Paolo","family":"Arcaini","sequence":"first","affiliation":[{"name":"Charles University, Faculty of Mathematics and Physics, Czech Republic"}]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano, Italy"}]},{"given":"Patrizia","family":"Scandurra","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Bergamo, Italy"}]}],"member":"320","published-online":{"date-parts":[[2017,1,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2494444.2494446"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2012.30"},{"volume-title":"From Model-Based Design to Formal Verification of Adaptive Embedded Systems","author":"Adler Rasmus","key":"e_1_2_1_3_1","unstructured":"Rasmus Adler , Ina Schaefer , Tobias Schuele , and Eric Vecchi\u00e9 . 2007. From Model-Based Design to Formal Verification of Adaptive Embedded Systems . Springer , Berlin , 76--95. Rasmus Adler, Ina Schaefer, Tobias Schuele, and Eric Vecchi\u00e9. 2007. From Model-Based Design to Formal Verification of Adaptive Embedded Systems. Springer, Berlin, 76--95."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053581"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_6"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 2nd NASA Formal Methods Symposium (NFM\u201910)","author":"Arcaini Paolo","year":"2010","unstructured":"Paolo Arcaini , Angelo Gargantini , and Elvinia Riccobene . 2010 b. Automatic review of abstract state machines by meta property verification . In Proceedings of the 2nd NASA Formal Methods Symposium (NFM\u201910) , NASA\/CP-2010-216215, C\u00e9sar Mu\u00f1oz (Ed.). NASA, Langley Research Center, Hampton VA, 4--13. Paolo Arcaini, Angelo Gargantini, and Elvinia Riccobene. 2010b. Automatic review of abstract state machines by meta property verification. In Proceedings of the 2nd NASA Formal Methods Symposium (NFM\u201910), NASA\/CP-2010-216215, C\u00e9sar Mu\u00f1oz (Ed.). NASA, Langley Research Center, Hampton VA, 4--13."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_17"},{"volume-title":"ABZ 2014: The Landing Gear Case Study, Fr\u00e9d\u00e9ric Boniol, Virginie Wiels, Yamine Ait Ameur, and Klaus-Dieter Schewe (Eds.). Communications in Computer and Information Science","author":"Arcaini Paolo","key":"e_1_2_1_8_1","unstructured":"Paolo Arcaini , Angelo Gargantini , and Elvinia Riccobene . 2014. Offline model-based testing and runtime monitoring of the sensor voting module . In ABZ 2014: The Landing Gear Case Study, Fr\u00e9d\u00e9ric Boniol, Virginie Wiels, Yamine Ait Ameur, and Klaus-Dieter Schewe (Eds.). Communications in Computer and Information Science , Vol. 433 . Springer International Publishing , 95--109. Paolo Arcaini, Angelo Gargantini, and Elvinia Riccobene. 2014. Offline model-based testing and runtime monitoring of the sensor voting module. In ABZ 2014: The Landing Gear Case Study, Fr\u00e9d\u00e9ric Boniol, Virginie Wiels, Yamine Ait Ameur, and Klaus-Dieter Schewe (Eds.). Communications in Computer and Information Science, Vol. 433. Springer International Publishing, 95--109."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 14th International Conference on Software Engineering and Formal Methods, held as part of STAF","author":"Arcaini Paolo","year":"2016","unstructured":"Paolo Arcaini , Angelo Gargantini , and Elvinia Riccobene . 2016a. SMT-based automatic proof of ASM model refinement . In Proceedings of the 14th International Conference on Software Engineering and Formal Methods, held as part of STAF 2016 , Rocco De Nicola and Eva K\u00fchn (Eds.). Springer International Publishing , Cham, 253--269. Paolo Arcaini, Angelo Gargantini, and Elvinia Riccobene. 2016a. SMT-based automatic proof of ASM model refinement. In Proceedings of the 14th International Conference on Software Engineering and Formal Methods, held as part of STAF 2016, Rocco De Nicola and Eva K\u00fchn (Eds.). Springer International Publishing, Cham, 253--269."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1019"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0371-5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2821357.2821362"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1988008.1988030"},{"volume-title":"Abstract State Machines 2003: Proceedings of the 10th International Workshop on Advances in Theory and Practice (ASM\u201903), Egon B\u00f6rger","author":"Beierle Christoph","key":"e_1_2_1_14_1","unstructured":"Christoph Beierle and Gabriele Kern-Isberner . 2003. Modelling conditional knowledge discovery and belief revision by abstract state machines . In Abstract State Machines 2003: Proceedings of the 10th International Workshop on Advances in Theory and Practice (ASM\u201903), Egon B\u00f6rger , Angelo Gargantini, and Elvinia Riccobene (Eds.). Springer , Berlin , 186--203. Christoph Beierle and Gabriele Kern-Isberner. 2003. Modelling conditional knowledge discovery and belief revision by abstract state machines. In Abstract State Machines 2003: Proceedings of the 10th International Workshop on Advances in Theory and Practice (ASM\u201903), Egon B\u00f6rger, Angelo Gargantini, and Elvinia Riccobene (Eds.). Springer, Berlin, 186--203."},{"volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"B\u00f6rger Egon","key":"e_1_2_1_15_1","unstructured":"Egon B\u00f6rger and Robert St\u00e4rk . 2003. Abstract State Machines: A Method for High-Level System Design and Analysis . Springer-Verlag . Egon B\u00f6rger and Robert St\u00e4rk. 2003. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02161-9_3"},{"key":"e_1_2_1_17_1","volume-title":"Alberto Lluch Lafuente, and Andrea Vandin","author":"Bruni Roberto","year":"2013","unstructured":"Roberto Bruni , Andrea Corradini , Fabio Gadducci , Alberto Lluch Lafuente, and Andrea Vandin . 2013 . Adaptable Transition Systems. Springer , Berlin, 95--110. Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, and Andrea Vandin. 2013. Adaptable Transition Systems. Springer, Berlin, 95--110."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.11.043"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Radu Calinescu Simos Gerasimou and Alec Banks. 2015. Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE\u201915) held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201915). Springer Berlin pp. 235--251.  Radu Calinescu Simos Gerasimou and Alec Banks. 2015. Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE\u201915) held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201915). Springer Berlin pp. 235--251.","DOI":"10.1007\/978-3-662-46675-9_16"},{"key":"e_1_2_1_20_1","first-page":"122","volume-title":"Revised Selected Papers. Springer","author":"Calinescu Radu","year":"2011","unstructured":"Radu Calinescu and Shinji Kikuchi . 2011 . Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems: 16th Monterey Workshop 2010 , Revised Selected Papers. Springer , Berlin , pp. 122 -- 135 . Radu Calinescu and Shinji Kikuchi. 2011. Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems: 16th Monterey Workshop 2010, Revised Selected Papers. Springer, Berlin, pp. 122--135."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2015.7381823"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.68"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_7"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02161-9_1"},{"key":"e_1_2_1_25_1","first-page":"67","article-title":"Software engineering for self-adaptive systems: Assurances (Dagstuhl seminar 13511)","volume":"3","author":"de Lemos Rogerio","year":"2014","unstructured":"Rogerio de Lemos , David Garlan , Carlo Ghezzi , and Holger Giese . 2014 . Software engineering for self-adaptive systems: Assurances (Dagstuhl seminar 13511) . Dagstuhl Rep. 3 , 12 (2014), 67 -- 96 . http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2014\/4508 Rogerio de Lemos, David Garlan, Carlo Ghezzi, and Holger Giese. 2014. Software engineering for self-adaptive systems: Assurances (Dagstuhl seminar 13511). Dagstuhl Rep. 3, 12 (2014), 67--96. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2014\/4508","journal-title":"Dagstuhl Rep."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02161-9_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETICE.2014.11"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025147"},{"volume-title":"Uncertainty in Self-Adaptive Software Systems","author":"Esfahani Naeem","key":"e_1_2_1_29_1","unstructured":"Naeem Esfahani and Sam Malek . 2013. Uncertainty in Self-Adaptive Software Systems . Springer , Berlin , 214--238. Naeem Esfahani and Sam Malek. 2013. Uncertainty in Self-Adaptive Software Systems. Springer, Berlin, 214--238."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11047-012-9324-y"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1675885"},{"key":"e_1_2_1_32_1","first-page":"1949","article-title":"A metamodel-based language and a simulation engine for abstract state machines","volume":"14","author":"Gargantini Angelo","year":"2008","unstructured":"Angelo Gargantini , Elvinia Riccobene , and Patrizia Scandurra . 2008 . A metamodel-based language and a simulation engine for abstract state machines . J. UCS 14 , 12 (2008), 1949 -- 1983 . Angelo Gargantini, Elvinia Riccobene, and Patrizia Scandurra. 2008. A metamodel-based language and a simulation engine for abstract state machines. J. UCS 14, 12 (2008), 1949--1983.","journal-title":"J. UCS"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/582128.582135"},{"volume-title":"Proceedings of the 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS\u201913)","author":"Didac","key":"e_1_2_1_34_1","unstructured":"Didac Gil de la Iglesia and Danny Weyns. 2013. Guaranteeing robustness in a mobile learning application using formally verified MAPE loops . In Proceedings of the 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS\u201913) . IEEE Press, 83--92. Didac Gil de la Iglesia and Danny Weyns. 2013. Guaranteeing robustness in a mobile learning application using formally verified MAPE loops. In Proceedings of the 8th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS\u201913). IEEE Press, 83--92."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2724719"},{"key":"e_1_2_1_36_1","first-page":"1","article-title":"Time in state machines","volume":"77","author":"Graf Susanne","year":"2007","unstructured":"Susanne Graf and Andreas Prinz . 2007 . Time in state machines . Fundam. Inf. 77 , 1 -- 2 (Jan. 2007), 143--174. Susanne Graf and Andreas Prinz. 2007. Time in state machines. Fundam. Inf. 77, 1--2 (Jan. 2007), 143--174.","journal-title":"Fundam. Inf."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2007.377861"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1380584.1380585"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.91.4"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593929.2593944"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1160055"},{"volume-title":"Proceedings of the 5th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY\u201904)","author":"Jeffrey","key":"e_1_2_1_42_1","unstructured":"Jeffrey O. Kephart and William E. Walsh. 2004. An artificial intelligence perspective on autonomic computing policies . In Proceedings of the 5th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY\u201904) . IEEE Computer Society, 3--12. Jeffrey O. Kephart and William E. Walsh. 2004. An artificial intelligence perspective on autonomic computing policies. In Proceedings of the 5th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY\u201904). IEEE Computer Society, 3--12."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.11.011"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1137677.1137684"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.91.8"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2013.11.002"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.09.017"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070514"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/375094.375118"},{"key":"e_1_2_1_50_1","volume-title":"Papadopoulos and Farhad Arbab","author":"George","year":"1998","unstructured":"George A. Papadopoulos and Farhad Arbab . 1998 . Coordination Models and Languages. Technical Report. Centre for Mathematics and Computer Science , Amsterdam, The Netherlands. George A. Papadopoulos and Farhad Arbab. 1998. Coordination Models and Languages. Technical Report. Centre for Mathematics and Computer Science, Amsterdam, The Netherlands."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568088.2568095"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SIES.2012.6356594"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28765-7_26"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41533-3_34"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1988008.1988037"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2347583.2347592"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1809049.1809078"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1808984.1808994"},{"key":"e_1_2_1_59_1","first-page":"76","volume-title":"G\u00f6schka","author":"Weyns Danny","year":"2013","unstructured":"Danny Weyns , Bradley R. Schmerl , Vincenzo Grassi , Sam Malek , Raffaela Mirandola , Christian Prehofer , Jochen Wuttke , Jesper Andersson , Holger Giese , and Karl M . G\u00f6schka . 2013 . Software Engineering for Self-Adaptive Systems II: International Seminar , 2010 Revised Selected and Invited Papers. Springer , Berlin, pp. 76 -- 107 . Danny Weyns, Bradley R. Schmerl, Vincenzo Grassi, Sam Malek, Raffaela Mirandola, Christian Prehofer, Jochen Wuttke, Jesper Andersson, Holger Giese, and Karl M. G\u00f6schka. 2013. Software Engineering for Self-Adaptive Systems II: International Seminar, 2010 Revised Selected and Invited Papers. Springer, Berlin, pp. 76--107."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.5555\/2666795.2666808"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134337"}],"container-title":["ACM Transactions on Autonomous and Adaptive Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3019598","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3019598","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:56Z","timestamp":1750220636000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3019598"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,10]]},"references-count":61,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,2,3]]}},"alternative-id":["10.1145\/3019598"],"URL":"https:\/\/doi.org\/10.1145\/3019598","relation":{},"ISSN":["1556-4665","1556-4703"],"issn-type":[{"type":"print","value":"1556-4665"},{"type":"electronic","value":"1556-4703"}],"subject":[],"published":{"date-parts":[[2017,1,10]]},"assertion":[{"value":"2015-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-01-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}