{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:11:28Z","timestamp":1746072688710,"version":"3.40.4"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908996","type":"print"},{"value":"9783031909009","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>It is often the case that a robot must adapt to unexpected changes in its environment. It is, however, important that these changes can be demonstrated to maintain the safe operation of the robot. The adaptive systems community has developed the MAPE-K pattern as a widely recognised conceptual architecture. We propose extending MAPE-K to incorporate runtime verification, resulting in an architecture we call MAPLE-K. In this paper, we capture and formalise both the MAPE-K and MAPLE-K architectures using a domain-specific language. Additionally, we provide support for translation from architectural models to software models and code to facilitate the deployment of verified applications. MAPE-K is rarely maintained at the implementation level, but our work ensures traceability between the code and its design, enabling the use of architectural information to verify the correctness of the software.\n\n<\/jats:p>","DOI":"10.1007\/978-3-031-90900-9_8","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:22Z","timestamp":1745988322000},"page":"145-165","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Architectural Patterns for Adaptive Robotic Software"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6083-9607","authenticated-orcid":false,"given":"James","family":"Baxter","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3854-5159","authenticated-orcid":false,"given":"Bert","family":"van Acker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8467-7567","authenticated-orcid":false,"given":"Morten","family":"Kristensen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8035-0884","authenticated-orcid":false,"given":"Thomas","family":"Wright","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0831-1976","authenticated-orcid":false,"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2692-9742","authenticated-orcid":false,"given":"Cl\u00e1udio","family":"Gomes","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"8_CR1","unstructured":"The ASMETA toolset website, https:\/\/asmeta.github.io\/"},{"key":"8_CR2","unstructured":"RoboArch, AADL and Turtlebot code (October 2024), https:\/\/drive.google.com\/file\/d\/1GafWyNsXQt7fX67SVfNrPbNTnvLXY9Tg"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Adaili, F., Mosbahi, O., Khalgui, M., Bouzefrane, S.: Ra2dl: New flexible solution for adaptive aadl-based control components. In: 2015 International Conference on Pervasive and Embedded Computing and Communication Systems (PECCS). pp. 247\u2013258 (2015)","DOI":"10.5220\/0005241202470258"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Arcaini, P., Riccobene, E., Scandurra, P.: Modeling and Analyzing MAPE-K Feedback Loops for Self-Adaptation. In: 2015 IEEE\/ACM 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems. pp. 13\u201323. IEEE, Florence, Italy (May 2015). https:\/\/doi.org\/10.1109\/SEAMS.2015.10","DOI":"10.1109\/SEAMS.2015.10"},{"key":"8_CR5","unstructured":"AS5506A, S.: Architecture analysis and design language (aadl) version 2.0. SAE: Warrendale, PA, USA (2009)"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Bagheri, M., Sirjani, M., Movaghar, A., Lee, E.A.: Coordinated actor model of self-adaptive track-based traffic control systems. The Journal of Systems & Software 143(September 2017), 116\u2013139 (2018). https:\/\/doi.org\/10.1016\/j.jss.2018.05.034","DOI":"10.1016\/j.jss.2018.05.034"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Barnett, W., Cavalcanti, A.L.C., Miyazawa, A.: Architectural Modelling for Robotics: RoboArch and the CorteX example. Frontiers of Robotics and AI (2022). https:\/\/doi.org\/10.3389\/frobt.2022.991637","DOI":"10.3389\/frobt.2022.991637"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Bonasso, R.P., Firby, R.J., Gat, E., Kortenkamp, D., Miller, D.P., Slack, M.G.: Experiences with an architecture for intelligent, reactive agents. Journal of Experimental and Theoretical Artificial Intelligence 9(2-3), 237\u2013256 (1997)","DOI":"10.1080\/095281397147103"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Bruni, R., Corradini, A., Gadducci, F., Lluch\u00a0Lafuente, A., Vandin, A.: A conceptual framework for adaptation. vol. 7212 LNCS, pp. 240\u2013254 (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_17","DOI":"10.1007\/978-3-642-28872-2_17"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Camilli, M., Bellettini, C., Capra, L.: A high-level petri net-based formal model of Distributed Self-adaptive Systems (2018). https:\/\/doi.org\/10.1145\/3241403.3241445","DOI":"10.1145\/3241403.3241445"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Cavalcanti, A.L.C., Barnett, W., Baxter, J., Carvalho, G., Filho, M.C., Miyazawa, A., Ribeiro, P., Sampaio, A.C.A.: RoboStar Technology: A Roboticist\u2019s Toolbox for Combined Proof, Simulation, and Testing, pp. 249\u2013293. Springer International Publishing (2021). https:\/\/doi.org\/10.1007\/978-3-030-66494-7_9, papers\/CBBCFMRS21.pdf","DOI":"10.1007\/978-3-030-66494-7_9"},{"key":"8_CR12","unstructured":"Feiler, P.: Open source aadl tool environment (osate). In: AADL Workshop, paris. pp. 1\u201340 (2004)"},{"key":"8_CR13","unstructured":"Feiler, P.H., Gluch, D.P.: Model-based engineering with AADL: an introduction to the SAE architecture analysis & design language. Addison-Wesley (2012)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Goncalves, F.S., Pereira, D., Tovar, E., Becker, L.B.: Formal verification of aadl models using uppaal. In: 2017 VII Brazilian Symposium on Computing Systems Engineering (SBESC). pp. 117\u2013124. IEEE (2017)","DOI":"10.1109\/SBESC.2017.22"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Hadad, A.S.A., Ma, C., Ahmed, A.A.O.: Formal verification of aadl models by event-b. IEEE Access 8, 72814\u201372834 (2020)","DOI":"10.1109\/ACCESS.2020.2987972"},{"key":"8_CR16","unstructured":"IBM: An architectural blueprint for autonomic computing. Tech. rep. (2005)"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Kephart, J., Chess, D.: The vision of autonomic computing. Computer 36(1), 41\u201350 (Jan 2003). https:\/\/doi.org\/10.1109\/MC.2003.1160055","DOI":"10.1109\/MC.2003.1160055"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Larsen, P.G., Ali, S., Behrens, R., Cavalcanti, A., Gomes, C., Li, G., De\u00a0Meulenaere, P., Olsen, M.L., Passalis, N., Peyrucain, T., et\u00a0al.: Robotic safe adaptation in unprecedented situations: the robosapiens project. Research Directions: Cyber-Physical Systems 2, \u00a0e4 (2024). https:\/\/doi.org\/10.1017\/cbp.2024.4","DOI":"10.1017\/cbp.2024.4"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A.L.C., Timmis, J., Woodcock, J.C.P.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Software & Systems Modeling 18(5), 3097\u20133149 (2019). https:\/\/doi.org\/10.1007\/s10270-018-00710-z, rdcu.be\/bh7dI","DOI":"10.1007\/s10270-018-00710-z"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Portocarrero, J., Delicato, F., Pires, P., Batista, T.: Reference architecture for self-adaptive management in wireless sensor networks. vol. 8779 LNAI, pp. 110\u2013120 (2014). https:\/\/doi.org\/10.1007\/978-3-319-11298-5_12","DOI":"10.1007\/978-3-319-11298-5_12"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science, Springer (2011)","DOI":"10.1007\/978-1-84882-258-0"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Weyns, D., Iftikhar, U.: ActivFORMS: A Formally Founded Model-based Approach to Engineer Self-adaptive Systems. ACM Transactions on Software Engineering and Methodology 32(1) (2023). https:\/\/doi.org\/10.1145\/3522585","DOI":"10.1145\/3522585"},{"key":"8_CR23","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z - Specification, Refinement, and Proof. Prentice-Hall (1996)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90900-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:29Z","timestamp":1745988329000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90900-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908996","9783031909009"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90900-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}