{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T10:40:08Z","timestamp":1750934408612,"version":"3.41.0"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T00:00:00Z","timestamp":1745366400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T00:00:00Z","timestamp":1745366400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100011914","name":"M\u00e4lardalen University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100011914","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":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper proposes an approach to pattern-based modeling and <jats:sc>Uppaal<\/jats:sc>-based verification for ROS 2 applications. The proposed verification focuses on callback execution latencies and buffer overflow. We propose formal model templates to model the execution of ROS 2 system components, created using a pattern-based approach. The model templates simplify the formal modeling of an ROS 2 application. Using <jats:sc>Uppaal<\/jats:sc>, we model in <jats:sc>Uppaal<\/jats:sc> timed automata, allowing the description of computation chains of ROS 2-based applications. Our focus is on execution behavior, including two versions of the mainline single-threaded executor of ROS 2. System traces generated using the formal models are validated in multiple experiments. Furthermore, we compare two approaches to modeling the execution of nodes that are typically the core units of computation of ROS 2. The first approach is a holistic approach to model ROS 2 applications, including communication and execution in computation chains. The second is an approach for individual nodes only, at a higher abstraction level. Additionally, we show the application of the verification by model checking in two ROS 2 system scenarios where we compare generated model traces to actual system executions. Overall, through formal modeling and verification, we showcase the potential for uncovering errors in the execution of distributed robotic systems.<\/jats:p>","DOI":"10.1007\/s10009-025-00802-4","type":"journal-article","created":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T13:54:55Z","timestamp":1745416495000},"page":"313-332","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Pattern-based verification of ROS 2 applications using UPPAAL"],"prefix":"10.1007","volume":"27","author":[{"given":"Lukas","family":"Dust","sequence":"first","affiliation":[]},{"given":"Rong","family":"Gu","sequence":"additional","affiliation":[]},{"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[]},{"given":"Mikael","family":"Ekstr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Saad","family":"Mubeen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,4,23]]},"reference":[{"key":"802_CR1","doi-asserted-by":"publisher","first-page":"917","DOI":"10.1007\/s00165-015-0340-4","volume":"27","author":"O. Al-Bataineh","year":"2015","unstructured":"Al-Bataineh, O., Reynolds, M., French, T.: Accelerating worst case execution time analysis of timed automata models with cyclic behaviour. Form. Asp. Comput. 27, 917\u2013949 (2015)","journal-title":"Form. Asp. Comput."},{"key":"802_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2022.111574","volume":"197","author":"M. Albonico","year":"2023","unstructured":"Albonico, M., Dordevic, M., Hamer, E., Malavolta, I.: Software engineering research on the robot operating system: a systematic mapping study. J. Syst. Softw. 197, Article ID\u00a0111574 (2023). https:\/\/doi.org\/10.1016\/j.jss.2022.111574","journal-title":"J. Syst. Softw."},{"key":"802_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"802_CR4","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-319-22102-1_3","volume-title":"Interactive Theorem Proving","author":"A. Anand","year":"2015","unstructured":"Anand, A., Knepper, R.: Roscoq: robots powered by constructive reals. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving, pp.\u00a034\u201350. Springer, Cham (2015)"},{"key":"802_CR5","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"802_CR6","first-page":"41","volume-title":"IEEE Real-Time Systems Symposium","author":"T. Bla\u00df","year":"2021","unstructured":"Bla\u00df, T., Casini, D., Bozhko, S., Brandenburg, B.B.: A ROS 2 response-time analysis exploiting starvation freedom and execution-time variance. In: IEEE Real-Time Systems Symposium, pp.\u00a041\u201353. IEEE Press, New York (2021)"},{"key":"802_CR7","volume-title":"2020 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS)","author":"R. Carvalho","year":"2020","unstructured":"Carvalho, R., Cunha, A., Macedo, N., Santos, A.: Verification of system-wide safety properties of ROS applications. In: 2020 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS) (2020)"},{"key":"802_CR8","first-page":"1","volume-title":"31st Euromicro Conference on Real-Time Systems","author":"D. Casini","year":"2019","unstructured":"Casini, D., Bla\u00df, T., L\u00fctkebohle, I., Brandenburg, B.: Response-time analysis of ROS 2 processing chains under reservation-based scheduling. In: 31st Euromicro Conference on Real-Time Systems, pp.\u00a01\u201323 (2019)"},{"key":"802_CR9","volume-title":"Proceedings of the 10th International Workshop on Worst-Case Execution-Time Analysis (WCET2010)","author":"A. Dalsgaard","year":"2010","unstructured":"Dalsgaard, A., Olesen, M., Toft, M., Hansen, R., Larsen, K.: METAMOC: modular execution time analysis using model checking. In: Proceedings of the 10th International Workshop on Worst-Case Execution-Time Analysis (WCET2010) (2010)"},{"key":"802_CR10","volume-title":"FMICS 2023 \u2013 International Conference on Formal Methods for Industrial Critical Systems","author":"L. Dust","year":"2023","unstructured":"Dust, L., Gu, R., Seceleanu, C., Ekstr\u00f6m, M., Mubeen, S.: Pattern-based verification of ROS 2 nodes using UPPAAL. In: FMICS 2023 \u2013 International Conference on Formal Methods for Industrial Critical Systems (2023)"},{"key":"802_CR11","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/FormaliSE.2017.9","volume-title":"2017 IEEE\/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE)","author":"R. Halder","year":"2017","unstructured":"Halder, R., Proen\u00e7a, J., Macedo, N., Santos, A.: Formal verification of ROS-based robotic applications using timed-automata. In: 2017 IEEE\/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp.\u00a044\u201350 (2017)"},{"key":"802_CR12","volume-title":"Third International Conference on the Quantitative Evaluation of Systems \u2013 (QEST\u201906)","author":"M. Hendriks","year":"2006","unstructured":"Hendriks, M., Yi, W., Petterson, P., Hakansson, J., Larsen, K., David, A., Behrmann, G.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems \u2013 (QEST\u201906) (2006)"},{"key":"802_CR13","unstructured":"OpenRobotics: Ros: Distributions (2023). http:\/\/wiki.ros.org\/Distributions"},{"key":"802_CR14","unstructured":"OpenRobotics: Ros 2: Distributions (2023). https:\/\/docs.ros.org\/en\/humble\/Releases"},{"key":"802_CR15","unstructured":"OpenRobotics: Ros 2: Documentation (2023). https:\/\/docs.ros.org\/en\/humble"},{"key":"802_CR16","first-page":"5","volume-title":"ICRA Workshop on Open Source Software","author":"M. Quigley","year":"2009","unstructured":"Quigley, M., Conley, K., Gerkey, B., Faust, J., Foote, T., Leibs, J., Wheeler, R., Ng, A.Y., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software, vol.\u00a03, pp.\u00a05. Kobe, Japan (2009)"},{"key":"802_CR17","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1145\/1837274.1837461","volume-title":"Proceedings of the 47th Design Automation Conference","author":"R. Rajkumar","year":"2010","unstructured":"Rajkumar, R., Lee, I., Sha, L., Stankovic, J.: Cyber-physical systems: the next computing revolution. In: Proceedings of the 47th Design Automation Conference, pp.\u00a0731\u2013736 (2010)"},{"key":"802_CR18","first-page":"231","volume-title":"IEEE Real-Time Systems Symposium","author":"Y. Tang","year":"2020","unstructured":"Tang, Y., Feng, Z., Guan, N., Jiang, X., Lv, M., Deng, Q., Yi, W.: Response time analysis and priority assignment of processing chains on ROS2 executors. In: IEEE Real-Time Systems Symposium, pp.\u00a0231\u2013243 (2020)"},{"key":"802_CR19","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1109\/RTSS55097.2022.00015","volume-title":"2022 IEEE Real-Time Systems Symposium (RTSS)","author":"H. Teper","year":"2022","unstructured":"Teper, H., G\u00fcnzel, M., Ueter, N., von der Br\u00fcggen, G., Chen, J.J.: End-to-end timing analysis in ROS 2. In: 2022 IEEE Real-Time Systems Symposium (RTSS), pp.\u00a053\u201365 (2022)"},{"issue":"2","key":"802_CR20","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1109\/THMS.2015.2425139","volume":"46","author":"M. Webster","year":"2016","unstructured":"Webster, M., Dixon, C., Fisher, M., Salem, M., Saunders, J., Koay, K.L., Dautenhahn, K., Saez-Pons, J.: Toward reliable autonomous robotic assistants through formal verification: a case study. IEEE Trans. Human-Mach. Syst. 46(2), 186\u2013196 (2016)","journal-title":"IEEE Trans. Human-Mach. Syst."}],"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-025-00802-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-025-00802-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00802-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T10:14:38Z","timestamp":1750932878000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-025-00802-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,23]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["802"],"URL":"https:\/\/doi.org\/10.1007\/s10009-025-00802-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2025,4,23]]},"assertion":[{"value":"3 April 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 April 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}