{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T10:17:52Z","timestamp":1768472272083,"version":"3.49.0"},"reference-count":66,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T00:00:00Z","timestamp":1698883200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T00:00:00Z","timestamp":1698883200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004434","name":"Universit\u00e0 degli Studi di Firenze","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004434","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Software development for robotics applications is still a major challenge that becomes even more complex when considering multi-robot systems (MRSs). Such distributed software has to perform multiple cooperating tasks in a well-coordinated manner to avoid unsatisfactory emerging behavior. This paper provides an approach for programming MRSs at a high abstraction level using the programming language <jats:sc>X-Klaim<\/jats:sc>. The computation and communication model of <jats:sc>X-Klaim<\/jats:sc>, based on multiple distributed tuple spaces, permits coordinating with the same abstractions and mechanisms both intra- and inter-robot interactions of an MRS. This allows developers to focus on MRS behavior, achieving readable, reusable, and maintainable code. The proposed approach can be used in practice by integrating <jats:sc>X-Klaim<\/jats:sc> and the popular robotics framework ROS. We demonstrate the feasibility and effectiveness of our approach by (i) showing how it scales when implementing two warehouse scenarios allowing us to reuse most of the code when passing from the simpler to the more enriched scenario and (ii) presenting the results of a few experiments showing that our code introduces a slightly greater but acceptable latency and consumes less memory than the traditional ROS implementation based on Python code.<\/jats:p>","DOI":"10.1007\/s10009-023-00727-w","type":"journal-article","created":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T13:02:13Z","timestamp":1698930133000},"page":"747-764","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Coordinating and programming multiple ROS-based robots with X-KLAIM"],"prefix":"10.1007","volume":"25","author":[{"given":"Lorenzo","family":"Bettini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khalid","family":"Bourr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rosario","family":"Pugliese","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Tiezzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,11,2]]},"reference":[{"key":"727_CR1","series-title":"LNCS","first-page":"149","volume-title":"Proc. of SIMPAR","author":"S. Dhouib","year":"2012","unstructured":"Dhouib, S., et al.: RobotML, a domain-specific language to design, simulate and deploy robotic applications. In: Proc. of SIMPAR. LNCS, vol.\u00a07628, pp.\u00a0149\u2013160. Springer, Berlin (2012)"},{"key":"727_CR2","unstructured":"Frigerio, M., Buchli, J., Caldwell, D.G.: A domain specific language for kinematic models and fast implementations of robot dynamics algorithms. In: Proc. of DSLRob\u201911. CoRR (2013). arXiv:1301.7190"},{"key":"727_CR3","first-page":"75","volume":"7","author":"A. Nordmann","year":"2016","unstructured":"Nordmann, A., Hochgeschwender, N., Wigand, D., Wrede, S.: A survey on domain-specific modeling and languages in robotics. Softw. Eng. Robot. 7, 75\u201399 (2016)","journal-title":"Softw. Eng. Robot."},{"key":"727_CR4","first-page":"1014","volume-title":"Int. Conf. on Computing, Communication, Automation","author":"R. Doriya","year":"2015","unstructured":"Doriya, R., Mishra, S., Gupta, S.: A brief survey and analysis of multi-robot communication and coordination. In: Int. Conf. on Computing, Communication, Automation, pp.\u00a01014\u20131021 (2015)"},{"key":"727_CR5","doi-asserted-by":"publisher","DOI":"10.3389\/frobt.2018.00094","volume":"5","author":"R. De Nicola","year":"2018","unstructured":"De Nicola, R., Di Stefano, L., Inverso, O.: Toward formal models and languages for verifiable multi-robot systems. Front. Robot. AI 5, 94 (2018)","journal-title":"Front. Robot. AI"},{"key":"727_CR6","volume-title":"ICRA Workshop on Open Source Software","author":"M. Quigley","year":"2009","unstructured":"Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software (2009)"},{"key":"727_CR7","series-title":"LNCS","first-page":"195","volume-title":"SIMPAR","author":"A. Nordmann","year":"2014","unstructured":"Nordmann, A., Hochgeschwender, N., Wrede, S.: A survey on domain-specific languages in robotics. In: SIMPAR. LNCS, vol.\u00a08810, pp.\u00a0195\u2013206. Springer, Berlin (2014)"},{"key":"727_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/j.cola.2020.101021","volume":"62","author":"E. de Ara\u00fajo Silva","year":"2021","unstructured":"de Ara\u00fajo Silva, E., Valentin, E., Carvalho, J.R.H., da Silva Barreto, R.: A survey of model driven engineering in robotics. Comput. Lang. 62, 101021 (2021)","journal-title":"Comput. Lang."},{"key":"727_CR9","doi-asserted-by":"crossref","unstructured":"Casalaro, G.L., et\u00a0al.: Model-driven engineering for mobile robotic systems: a systematic mapping study. Softw. Syst. Model. (2021)","DOI":"10.1007\/s10270-021-00908-8"},{"key":"727_CR10","series-title":"LNCS","first-page":"361","volume-title":"ISoLA 2020","author":"L. Bettini","year":"2020","unstructured":"Bettini, L., Bourr, K., Pugliese, R., Tiezzi, F.: Writing robotics applications with X-Klaim. In: ISoLA 2020. LNCS, vol.\u00a012477, pp.\u00a0361\u2013379. Springer, Heidelberg (2020)"},{"key":"727_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-21485-2_8","volume-title":"Models, Languages, and Tools for Concurrent and Distributed Programming","author":"L. Bettini","year":"2019","unstructured":"Bettini, L., Merelli, E., Tiezzi, F.: X-Klaim is back. In: Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol.\u00a011665, pp.\u00a0115\u2013135. Springer, Berlin (2019)"},{"key":"727_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-031-19759-8_18","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning","author":"L. Bettini","year":"2022","unstructured":"Bettini, L., Bourr, K., Pugliese, R., Tiezzi, F.: Programming multi-robot systems with X-Klaim. In: Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning. LNCS, vol.\u00a013703, pp.\u00a0283\u2013300. Springer, Berlin (2022)"},{"issue":"5","key":"727_CR13","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1109\/32.685256","volume":"24","author":"R. De Nicola","year":"1998","unstructured":"De Nicola, R., Ferrari, G.L., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE Trans. Softw. Eng. 24(5), 315\u2013330 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"727_CR14","volume-title":"Communication and Concurrency. PHI Series in Computer Science","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, New York (1989)"},{"issue":"1","key":"727_CR15","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/2363.2433","volume":"7","author":"D. Gelernter","year":"1985","unstructured":"Gelernter, D.: Generative communication in Linda. ACM Trans. Program. Lang. Syst. 7(1), 80\u2013112 (1985)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"14","key":"727_CR16","doi-asserted-by":"publisher","first-page":"1365","DOI":"10.1002\/spe.486","volume":"32","author":"L. Bettini","year":"2002","unstructured":"Bettini, L., De Nicola, R., Pugliese, R.: Klava: a Java package for distributed and mobile applications. Softw. Pract. Exp. 32(14), 1365\u20131394 (2002)","journal-title":"Softw. Pract. Exp."},{"key":"727_CR17","series-title":"LNCS","first-page":"181","volume-title":"DAIS","author":"L. Bettini","year":"2005","unstructured":"Bettini, L., De Nicola, R., Falassi, D., Lacoste, M., Loreti, M.: A flexible and modular framework for implementing infrastructures for global computing. In: DAIS. LNCS, vol.\u00a03543, pp.\u00a0181\u2013193. Springer, Berlin (2005)"},{"key":"727_CR18","first-page":"110","volume-title":"WETICE","author":"L. Bettini","year":"1998","unstructured":"Bettini, L., De Nicola, R., Pugliese, R., Ferrari, G.L.: Interactive mobile agents in X-Klaim. In: WETICE, pp.\u00a0110\u2013117. IEEE Computer Society, Los Alamitos (1998)"},{"key":"727_CR19","volume-title":"Implementing Domain-Specific Languages with Xtext and Xtend","author":"L. Bettini","year":"2016","unstructured":"Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend, 2nd edn. Packt Publishing (2016)","edition":"2"},{"key":"727_CR20","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1145\/2371401.2371419","volume-title":"GPCE","author":"S. Efftinge","year":"2012","unstructured":"Efftinge, S., Eysholdt, M., K\u00f6hnlein, J., Zarnekow, S., von Massow, R., Hasselbring, W., Hanus, M.: Xbase: implementing domain-specific languages for Java. In: GPCE, pp.\u00a0112\u2013121. ACM, New York (2012)"},{"key":"727_CR21","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1145\/508791.508862","volume-title":"SAC","author":"L. Bettini","year":"2002","unstructured":"Bettini, L., Loreti, M., Pugliese, R.: An infrastructure language for open nets. In: SAC, pp.\u00a0373\u2013377. ACM, New York (2002)"},{"key":"727_CR22","first-page":"2149","volume-title":"IROS","author":"N.P. Koenig","year":"2004","unstructured":"Koenig, N.P., Howard, A.: Design and use paradigms for Gazebo, an open-source multi-robot simulator. In: IROS, pp.\u00a02149\u20132154. IEEE Press, New York (2004)"},{"issue":"1\u20134","key":"727_CR23","doi-asserted-by":"publisher","first-page":"1195","DOI":"10.1007\/s00170-018-1976-z","volume":"97","author":"E. Est\u00e9vez","year":"2018","unstructured":"Est\u00e9vez, E., et al.: ART2ool: a model-driven framework to generate target code for robot handling tasks. Adv. Manuf. Technol. 97(1\u20134), 1195\u20131207 (2018)","journal-title":"Adv. Manuf. Technol."},{"key":"727_CR24","volume-title":"24th Int. Conf. on Model Driven Engineering Languages and Systems (MODELS)","author":"J. Harbin","year":"2021","unstructured":"Harbin, J., et al.: Model-driven simulation-based analysis for multi-robot systems. In: 24th Int. Conf. on Model Driven Engineering Languages and Systems (MODELS) (2021)"},{"key":"727_CR25","first-page":"137","volume-title":"ISR","author":"A. Bubeck","year":"2014","unstructured":"Bubeck, A., et al.: BRIDE - a toolchain for framework-independent development of industrial service robot applications. In: ISR, pp.\u00a0137\u2013142. VDE, (2014)"},{"key":"727_CR26","first-page":"433","volume-title":"Proc. of MODELS18 Workshops. CEUR Workshop Proc.","author":"A. Rutle","year":"2018","unstructured":"Rutle, A., Backer, J., Fold\u00f8y, K., Bye, R.T.: CommonLang: A DSL for defining robot tasks. In: Proc. of MODELS18 Workshops. CEUR Workshop Proc., vol.\u00a02245, pp.\u00a0433\u2013442 (2018)"},{"key":"727_CR27","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1145\/3055004.3055022","volume-title":"8th Intern. Conference on Cyber-Physical Systems","author":"A. Desai","year":"2017","unstructured":"Desai, A., Saha, I., Yang, J., Qadeer, S., Seshia, S.A.: Drona: a framework for safe distributed mobile robotics. In: 8th Intern. Conference on Cyber-Physical Systems, pp.\u00a0239\u2013248 (2017)"},{"key":"727_CR28","doi-asserted-by":"publisher","first-page":"6451","DOI":"10.1109\/ACCESS.2016.2613642","volume":"4","author":"F. Ciccozzi","year":"2016","unstructured":"Ciccozzi, F., et al.: Adopting MDE for specifying and executing civilian missions of mobile multi-robot systems. IEEE Access 4, 6451\u20136466 (2016)","journal-title":"IEEE Access"},{"key":"727_CR29","first-page":"509","volume-title":"Robot Operating System. Studies in Computational Intelligence","author":"D. Brugali","year":"2016","unstructured":"Brugali, D., Gherardi, L.: Hyperflex: a model driven toolchain for designing and configuring software control systems for autonomous robots. In: Robot Operating System. Studies in Computational Intelligence, vol.\u00a0625, pp.\u00a0509\u2013534. Springer, Berlin (2016)"},{"issue":"1","key":"727_CR30","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A. Lomuscio","year":"2017","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: Mcmas: an open-source model checker for the verification of multi-agent systems. Softw. Tools Technol. Transf. 19(1), 9\u201330 (2017)","journal-title":"Softw. Tools Technol. Transf."},{"issue":"OOPSLA","key":"727_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3428300","volume":"4","author":"R. Ghosh","year":"2020","unstructured":"Ghosh, R., et al.: Koord: a language for programming and verifying distributed robotics application. Proc. ACM Program. Lang. 4(OOPSLA), 1\u201330 (2020)","journal-title":"Proc. ACM Program. Lang."},{"key":"727_CR32","first-page":"127","volume-title":"12th ACM SIGPLAN Int. Conf on Software Language Engineering","author":"S. Garc\u00eda","year":"2019","unstructured":"Garc\u00eda, S., et al.: High-level mission specification for multiple robots. In: 12th ACM SIGPLAN Int. Conf on Software Language Engineering, pp.\u00a0127\u2013140 (2019)"},{"issue":"5","key":"727_CR33","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A. Miyazawa","year":"2019","unstructured":"Miyazawa, A., et al.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5), 3097\u20133149 (2019)","journal-title":"Softw. Syst. Model."},{"key":"727_CR34","unstructured":"St-Onge, D., Varadharajan, V.S., Li, G., Svogor, I., Beltrame, G.: ROS and Buzz: consensus-based behaviors for heterogeneous teams CoRR (2017). arXiv:1710.08843"},{"key":"727_CR35","doi-asserted-by":"publisher","first-page":"71617","DOI":"10.1109\/ACCESS.2020.2987099","volume":"8","author":"M. Figat","year":"2020","unstructured":"Figat, M., Zieli\u0144ski, C.: Robotic system specification methodology based on hierarchical Petri nets. IEEE Access 8, 71617\u201371627 (2020)","journal-title":"IEEE Access"},{"issue":"2","key":"727_CR36","doi-asserted-by":"publisher","DOI":"10.1145\/2619998","volume":"9","author":"R. De Nicola","year":"2014","unstructured":"De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL language. ACM Trans. Auton. Adapt. Syst. 9(2), 7 (2014)","journal-title":"ACM Trans. Auton. Adapt. Syst."},{"key":"727_CR37","first-page":"3","volume":"1","author":"D. Alonso","year":"2010","unstructured":"Alonso, D., et al.: V3CMM: a 3-view component meta-model for model-driven robotic software development. J. Softw. Eng. Robot. 1, 3\u201317 (2010)","journal-title":"J. Softw. Eng. Robot."},{"key":"727_CR38","first-page":"1758","volume-title":"SAC","author":"H. Bruyninckx","year":"2013","unstructured":"Bruyninckx, H., et al.: The BRICS component model: a model-based development paradigm for complex robotics software systems. In: SAC, pp.\u00a01758\u20131764. ACM, New York (2013)"},{"key":"727_CR39","first-page":"131","volume-title":"Proc. of CTS","author":"A. Ramaswamy","year":"2014","unstructured":"Ramaswamy, A., Monsuez, B., Tapus, A.: SafeRobots: A\u00a0model-driven approach for designing robotic software architectures. In: Proc. of CTS, pp.\u00a0131\u2013134. IEEE, New York (2014)"},{"key":"727_CR40","volume-title":"Int. Symp. on Rapid System Prototyping (RSP)","author":"P. Kumar","year":"2015","unstructured":"Kumar, P., et al.: ROSMOD: a toolsuite for modeling, generating, deploying, and managing distributed real-time component-based software using ROS. In: Int. Symp. on Rapid System Prototyping (RSP) (2015)"},{"key":"727_CR41","volume-title":"Workshop on Domain-Specific Languages and Models for Robotic Systems","author":"S. Adam","year":"2014","unstructured":"Adam, S., Schultz, U.P.: Towards interactive, incremental programming of ROS nodes. In: Workshop on Domain-Specific Languages and Models for Robotic Systems (2014)"},{"key":"727_CR42","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-319-17524-9_18","volume-title":"NASA Formal Methods Symposium","author":"W. Meng","year":"2015","unstructured":"Meng, W., Park, J., Sokolsky, O., Weirich, S., Lee, I.: Verified ROS-based deployment of platform-independent control systems. In: NASA Formal Methods Symposium, pp.\u00a0248\u2013262. Springer, Berlin (2015)"},{"issue":"1","key":"727_CR43","first-page":"121","volume":"7","author":"S. Adam","year":"2016","unstructured":"Adam, S., Larsen, M., Jensen, K., Schultz, U.P.: Rule-based dynamic safety monitoring for mobile robots. J. Softw. Eng. Robot. 7(1), 121\u2013141 (2016)","journal-title":"J. Softw. Eng. Robot."},{"key":"727_CR44","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-11164-3_20","volume-title":"Int. Conf. on Runtime Verification","author":"J. Huang","year":"2014","unstructured":"Huang, J., et al.: ROSRV: runtime verification for robots. In: Int. Conf. on Runtime Verification, pp.\u00a0247\u2013254. Springer, Berlin (2014)"},{"issue":"1","key":"727_CR45","doi-asserted-by":"publisher","first-page":"1096","DOI":"10.1109\/JSYST.2018.2867285","volume":"13","author":"R. Wang","year":"2018","unstructured":"Wang, R., Guan, Y., Song, H., Li, X., Li, X., Shi, Z., Song, X.: A formal model-based design method for robotic systems. IEEE Syst. J. 13(1), 1096\u20131107 (2018)","journal-title":"IEEE Syst. J."},{"key":"727_CR46","series-title":"LNCS","first-page":"45","volume-title":"SERENE","author":"S. Dragule","year":"2017","unstructured":"Dragule, S., Meyers, B., Pelliccione, P.: A generated property specification language for resilient multirobot missions. In: SERENE. LNCS, vol.\u00a010479, pp.\u00a045\u201361. Springer, Berlin (2017)"},{"issue":"2","key":"727_CR47","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1109\/TR.2019.2923681","volume":"69","author":"C. Hu","year":"2019","unstructured":"Hu, C., Dong, W., Yang, Y., Shi, H., Zhou, G.: Runtime verification on hierarchical properties of ROS-based robot swarms. IEEE Trans. Reliab. 69(2), 674\u2013689 (2019)","journal-title":"IEEE Trans. Reliab."},{"key":"727_CR48","doi-asserted-by":"publisher","DOI":"10.5772\/57313","volume":"10","author":"Z. Yan","year":"2013","unstructured":"Yan, Z., Jouandeau, N., Ali, A.: A survey and analysis of multi-robot coordination. Int. J. Adv. Robot. Syst. 10, 1 (2013)","journal-title":"Int. J. Adv. Robot. Syst."},{"issue":"5","key":"727_CR49","doi-asserted-by":"publisher","first-page":"2015","DOI":"10.1109\/TSMCB.2004.832155","volume":"34","author":"A. Farinelli","year":"2004","unstructured":"Farinelli, A., Iocchi, L., Nardi, D.: Multirobot systems: a classification focused on coordination. IEEE Trans. Syst. Man Cybern., Part B, Cybern. 34(5), 2015\u20132028 (2004)","journal-title":"IEEE Trans. Syst. Man Cybern., Part B, Cybern."},{"issue":"9","key":"727_CR50","volume":"2","author":"C. Pinciroli","year":"2016","unstructured":"Pinciroli, C., Lee-Brown, A., Beltrame, G.: A tuple space for data sharing in robot swarms. EAI Endorsed Trans. Collab. Comput. 2(9), 2 (2016)","journal-title":"EAI Endorsed Trans. Collab. Comput."},{"issue":"OOPSLA","key":"727_CR51","doi-asserted-by":"publisher","DOI":"10.1145\/3428202","volume":"4","author":"R. Majumdar","year":"2020","unstructured":"Majumdar, R., Yoshida, N., Zufferey, D.: Multiparty motion coordination: from choreographies to robotics programs. Proc. ACM Program. Lang. 4(OOPSLA), 134 (2020)","journal-title":"Proc. ACM Program. Lang."},{"key":"727_CR52","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3342355","volume":"52","author":"M. Luckcuck","year":"2020","unstructured":"Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems. ACM Comput. Surv. 52, 1\u201341 (2020)","journal-title":"ACM Comput. Surv."},{"issue":"1","key":"727_CR53","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/S0304-3975(99)00232-7","volume":"240","author":"R. De Nicola","year":"2000","unstructured":"De Nicola, R., Ferrari, G.L., Pugliese, R., Venneri, B.: Types for access control. Theor. Comput. Sci. 240(1), 215\u2013254 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"727_CR54","series-title":"LNCS","first-page":"86","volume-title":"SPC","author":"D. Gorla","year":"2003","unstructured":"Gorla, D., Pugliese, R.: Enforcing security policies via types. In: SPC. LNCS, vol.\u00a02802, pp.\u00a086\u2013100. Springer, Berlin (2003)"},{"key":"727_CR55","series-title":"LNCS","first-page":"119","volume-title":"ICALP","author":"D. Gorla","year":"2003","unstructured":"Gorla, D., Pugliese, R.: Resource access and mobility control with dynamic privileges acquisition. In: ICALP. LNCS, vol.\u00a02719, pp.\u00a0119\u2013132. Springer, Berlin (2003)"},{"issue":"1","key":"727_CR56","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.scico.2005.07.013","volume":"63","author":"R. De Nicola","year":"2006","unstructured":"De Nicola, R., Gorla, D., Pugliese, R.: Confining data and processes in global computing applications. Sci. Comput. Program. 63(1), 57\u201387 (2006)","journal-title":"Sci. Comput. Program."},{"issue":"10","key":"727_CR57","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1016\/j.ic.2007.03.004","volume":"205","author":"R. De Nicola","year":"2007","unstructured":"De Nicola, R., Gorla, D., Pugliese, R.: Basic observables for a calculus for global computing. Inf. Comput. 205(10), 1491\u20131525 (2007)","journal-title":"Inf. Comput."},{"issue":"6","key":"727_CR58","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.scico.2009.07.009","volume":"75","author":"R. De Nicola","year":"2010","unstructured":"De Nicola, R., et al.: From flow logic to static type systems for coordination languages. Sci. Comput. Program. 75(6), 376\u2013397 (2010)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"727_CR59","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/963927.963930","volume":"5","author":"R. De Nicola","year":"2004","unstructured":"De Nicola, R., Loreti, M.: A modal logic for mobile agents. ACM Trans. Comput. Log. 5(1), 79\u2013128 (2004)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"727_CR60","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2007.05.008","volume":"382","author":"R. De Nicola","year":"2007","unstructured":"De Nicola, R., Katoen, J., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theor. Comput. Sci. 382(1), 42\u201370 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"727_CR61","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.scico.2014.10.001","volume":"99","author":"J. Eckhardt","year":"2015","unstructured":"Eckhardt, J., M\u00fchlbauer, T., Meseguer, J., Wirsing, M.: Semantics, distributed implementation, and formal analysis of KLAIM models in Maude. Sci. Comput. Program. 99, 24\u201374 (2015)","journal-title":"Sci. Comput. Program."},{"key":"727_CR62","series-title":"LNCS","first-page":"54","volume-title":"ICFEM12","author":"E. Gjondrekaj","year":"2012","unstructured":"Gjondrekaj, E., et al.: Towards a formal verification methodology for collective robotic systems. In: ICFEM12. LNCS, vol.\u00a07635, pp.\u00a054\u201370. Springer, Berlin (2012)"},{"key":"727_CR63","series-title":"LNCS","first-page":"281","volume-title":"TACAS 2019","author":"G. Belmonte","year":"2019","unstructured":"Belmonte, G., Ciancia, V., Latella, D., Massink, M.: VoxLogicA: A spatial model checker for declarative image analysis. In: TACAS 2019. LNCS, vol.\u00a011427, pp.\u00a0281\u2013298. Springer, Berlin (2019)"},{"key":"727_CR64","series-title":"LNCS","first-page":"142","volume-title":"ISoLA 2022","author":"D. Basile","year":"2022","unstructured":"Basile, D., ter Beek, M.H., Ciancia, V.: An experimental toolchain for strategy synthesis with spatial properties. In: ISoLA 2022. LNCS, vol.\u00a013703, pp.\u00a0142\u2013164. Springer, Berlin (2022)"},{"issue":"3","key":"727_CR65","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10009-018-0483-8","volume":"20","author":"V. Ciancia","year":"2018","unstructured":"Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Int. J. Softw. Tools Technol. Transf. 20(3), 289\u2013311 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"727_CR66","first-page":"1522","volume-title":"SAC12","author":"E. Gjondrekaj","year":"2012","unstructured":"Gjondrekaj, E., Loreti, M., Pugliese, R., Tiezzi, F.: Modeling adaptation with a tuple-based coordination language. In: SAC12, pp.\u00a01522\u20131527. ACM, New York (2012)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00727-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-023-00727-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00727-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T14:07:19Z","timestamp":1701094039000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-023-00727-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,2]]},"references-count":66,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["727"],"URL":"https:\/\/doi.org\/10.1007\/s10009-023-00727-w","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,11,2]]},"assertion":[{"value":"10 October 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that the research was conducted in the absence of any commercial or financial relationships that could be construed as a potential conflict of interest. All authors contributed equally to this work.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}}]}}