{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T13:29:34Z","timestamp":1780493374332,"version":"3.54.1"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,9,1]],"date-time":"2015-09-01T00:00:00Z","timestamp":1441065600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Auton. Adapt. Syst."],"published-print":{"date-parts":[[2015,10,8]]},"abstract":"<jats:p>Designing software systems that have to deal with dynamic operating conditions, such as changing availability of resources and faults that are difficult to predict, is complex. A promising approach to handle such dynamics is self-adaptation that can be realized by a MAPE-K feedback loop (Monitor-Analyze-Plan-Execute plus Knowledge). To provide evidence that the system goals are satisfied, given the changing conditions, the state of the art advocates the use of formal methods. However, little research has been done on consolidating design knowledge of self-adaptive systems. To support designers, this paper contributes with a set of formally specified MAPE-K templates that encode design expertise for a family of self-adaptive systems. The templates comprise: (1) behavior specification templates for modeling the different components of a MAPE-K feedback loop (based on networks of timed automata), and (2) property specification templates that support verification of the correctness of the adaptation behaviors (based on timed computation tree logic). To demonstrate the reusability of the formal templates, we performed four case studies in which final-year Masters students used the templates to design different self-adaptive systems.<\/jats:p>","DOI":"10.1145\/2724719","type":"journal-article","created":{"date-parts":[[2015,9,8]],"date-time":"2015-09-08T12:36:15Z","timestamp":1441715775000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":106,"title":["MAPE-K Formal Templates to Rigorously Design Behaviors for Self-Adaptive Systems"],"prefix":"10.1145","volume":"10","author":[{"given":"Didac Gil De La","family":"Iglesia","sequence":"first","affiliation":[{"name":"Linnaeus University, V\u00e4xj\u00f6, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Danny","family":"Weyns","sequence":"additional","affiliation":[{"name":"Linnaeus University, V\u00e4xj\u00f6, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/21.87078"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"J.\n      Bengtsson\n     and \n      W.\n      Yi\n  . \n  2004\n  . Timed automata: Semantics algorithms and tools. In Lecture Notes on Concurrency and Petri Nets Lecture Notes in Computer Science Vol. \n  3098\n  . W. Reisig and G. Rozenberg (Eds.). \n  Springer-Verlag Berlin.  J. Bengtsson and W. Yi. 2004. Timed automata: Semantics algorithms and tools. In Lecture Notes on Concurrency and Petri Nets Lecture Notes in Computer Science Vol. 3098. W. Reisig and G. Rozenberg (Eds.). Springer-Verlag Berlin.","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"e_1_2_2_4_1","volume-title":"International Conference on Software Engineering. IEEE, 968--976","author":"Bianculli D."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02161-9_1"},{"key":"e_1_2_2_6_1","first-page":"12","article-title":"Software engineering for self-adaptive systems: Assurances (Dagstuhl Seminar 13511)","volume":"3","author":"de Lemos R.","year":"2014","journal-title":"Dagstuhl Reports"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02161-9_1"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1186778.1186782"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298598"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEAMS.2009.5069083"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025147"},{"key":"e_1_2_2_12_1","volume-title":"4th European Conference on Software Architecture. Springer, 8.","author":"Esfahani N."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0207-2"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2004.175"},{"key":"e_1_2_2_15_1","volume-title":"Assurances for Self-Adaptive Systems. Lecture Notes in Computer Science","volume":"7740","author":"Giese H."},{"key":"e_1_2_2_16_1","volume-title":"A Formal Approach for Designing Distributed Self-Adaptive Systems","author":"de la Iglesia D. Gil"},{"key":"e_1_2_2_17_1","volume-title":"Retrieved","author":"de la Iglesia D. Gil","year":"2015"},{"key":"e_1_2_2_18_1","volume-title":"International Symposium on Software Engineering for Adaptive and Self-Managing Systems. 83--92","author":"de la Iglesia D. Gil"},{"key":"e_1_2_2_19_1","volume-title":"International Conference on Autonomous Agents and Multi-agent Systems (AAMAS\u201913)","author":"de la Iglesia D. Gil","year":"2013"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1774088.1774185"},{"key":"e_1_2_2_21_1","volume-title":"4th Working IEEE\/IFIP Conference on Software Architecture (WICSA\u201904)","author":"Gomaa H."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368094"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"M. U. Iftikhar and D. Weyns. 2012. A case study on formal verification of self-adaptive behaviors in a decentralized system. In Foundations of Coordination Languages and Self Adaptation (FOCLASA\u201912).  M. U. Iftikhar and D. Weyns. 2012. A case study on formal verification of self-adaptive behaviors in a decentralized system. In Foundations of Coordination Languages and Self Adaptation (FOCLASA\u201912).","DOI":"10.4204\/EPTCS.91.4"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593929.2593944"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2591062.2591137"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1160055"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOSE.2007.19"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1137677.1137684"},{"key":"e_1_2_2_31_1","unstructured":"M. B. Miles and A. M. Huberman. 1994. Qualitative data analysis: An expanded sourcebook. SAGE Thousand Oaks CA.  M. B. Miles and A. M. Huberman. 1994. Qualitative data analysis: An expanded sourcebook. SAGE Thousand Oaks CA."},{"key":"e_1_2_2_32_1","volume-title":"20th International Conference on Software Engineering (ICSE\u201998)","author":"Oreizy P."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1808984.1808990"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2006.58"},{"key":"e_1_2_2_35_1","doi-asserted-by":"crossref","unstructured":"G. Tamura N. M. Villegas H. Muller J. P. Sousa B. Becker G. Karsai S. Mankovskii M. Pezze W. Schafer L. Tahvildari and K. Wong. 2012. Towards practical runtime verification and validation of self-adaptive software systems. Software Engineering for Self-Adaptive Systems II Springer.  G. Tamura N. M. Villegas H. Muller J. P. Sousa B. Becker G. Karsai S. Mankovskii M. Pezze W. Schafer L. Tahvildari and K. Wong. 2012. Towards practical runtime verification and validation of self-adaptive software systems. Software Engineering for Self-Adaptive Systems II Springer.","DOI":"10.1007\/978-3-642-35813-5_5"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.174"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2347583.2347592"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2168260.2168268"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/2487336.2487341"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"D. Weyns B. Schmerl V. Grassi S. Malek R. Mirandola C. Prehofer J. Wuttke J. Andersson H. Giese and K. Goeschka. 2013b. On patterns for decentralized control in self-adaptive systems. In Software Engineering for Self-Adaptive Systems II. Springer 76--107.  D. Weyns B. Schmerl V. Grassi S. Malek R. Mirandola C. Prehofer J. Wuttke J. Andersson H. Giese and K. Goeschka. 2013b. On patterns for decentralized control in self-adaptive systems. In Software Engineering for Self-Adaptive Systems II. Springer 76--107.","DOI":"10.1007\/978-3-642-35813-5_4"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SASO.2014.23"},{"key":"e_1_2_2_42_1","volume-title":"Case study research: Design and methods","author":"Yin Robert K."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134337"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1509239.1509262"}],"container-title":["ACM Transactions on Autonomous and Adaptive Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2724719","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2724719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:12Z","timestamp":1750227132000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2724719"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,10,8]]}},"alternative-id":["10.1145\/2724719"],"URL":"https:\/\/doi.org\/10.1145\/2724719","relation":{},"ISSN":["1556-4665","1556-4703"],"issn-type":[{"value":"1556-4665","type":"print"},{"value":"1556-4703","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9]]},"assertion":[{"value":"2014-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}