{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T01:29:42Z","timestamp":1772501382835,"version":"3.50.1"},"reference-count":33,"publisher":"Frontiers Media SA","license":[{"start":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T00:00:00Z","timestamp":1752624000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["frontiersin.org"],"crossmark-restriction":true},"short-container-title":["Front. Robot. AI"],"abstract":"<jats:p>Formal verification of robotic applications, particularly those based on ROS 2, is desirable for ensuring correctness and safety. However, the complexity of formal methods and the manual effort required for model creation and parameter extraction often hinder their adoption. This paper addresses these challenges by proposing a model-based methodology that automates the formal verification process using model-driven engineering techniques. We introduce a methodology which can be applied as a toolchain that automates the initialization of formal model templates in UPPAAL using system parameters derived from ROS 2 execution traces generated by the ROS2_tracing tool. The toolchain employs four model representations based on custom Eclipse Ecore metamodels to capture both structural and verification aspects of ROS 2 systems. The methodology supports both implemented and conceptual systems and enables iterative verification of timing and scheduling parameters through model-to-model and model-to-text transformations. A proof-of-concept implementation demonstrates the feasibility of the proposed approach. The designed toolchain supports verification using two types of UPPAAL models: one for individual node verification (e.g., callback latency and buffer overflow) and another for end-to-end latency analysis of ROS 2 processing chains. Experiments conducted on two implemented and one conceptual ROS 2 systems validate the correctness and adaptability of the toolchain. The results show that the toolchain can automate parameter extraction and model generation. The proposed methodology modularizes the verification process, allowing domain experts to focus on their areas of expertise. It targets to enhances traceability and reusability across different verification scenarios and formal models. The approach aims to make formal verification more accessible and practical to robotics developers.<\/jats:p>","DOI":"10.3389\/frobt.2025.1592523","type":"journal-article","created":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T12:28:07Z","timestamp":1752668887000},"update-policy":"https:\/\/doi.org\/10.3389\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A model-based approach to automation of formal verification of ROS 2-based systems"],"prefix":"10.3389","volume":"12","author":[{"given":"Lukas","family":"Dust","sequence":"first","affiliation":[]},{"given":"Rong","family":"Gu","sequence":"additional","affiliation":[]},{"given":"Saad","family":"Mubeen","sequence":"additional","affiliation":[]},{"given":"Mikael","family":"Ekstr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[]}],"member":"1965","published-online":{"date-parts":[[2025,7,16]]},"reference":[{"key":"B1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theor. Comput. Sci."},{"key":"B2","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/978-3-319-22102-1_3","article-title":"Roscoq: robots powered by constructive reals","volume-title":"Interactive theorem proving","author":"Anand","year":"2015"},{"key":"B3","unstructured":"Autoware: open-source software stack for autonomous driving\n          \n          \n          2025"},{"key":"B4","first-page":"95","article-title":"A model-driven software development approach using omg dds for wireless sensor networks","volume-title":"IFIP international workshop on software technolgies for embedded and ubiquitous systems","author":"Beckmann","year":"2010"},{"key":"B5","doi-asserted-by":"publisher","first-page":"104361","DOI":"10.1016\/j.robot.2022.104361","article-title":"Message flow analysis with complex causal links for distributed ros 2 systems","volume":"161","author":"B\u00e9dard","year":"2023","journal-title":"Robot. Aut. Syst."},{"key":"B6","doi-asserted-by":"publisher","first-page":"6511","DOI":"10.1109\/lra.2022.3174346","article-title":"ros2_tracing: multipurpose low-overhead framework for real-time tracing of ros 2","volume":"7","author":"B\u00e9dard","year":"2022","journal-title":"IEEE Robot. Autom. Lett."},{"key":"B7","doi-asserted-by":"crossref","DOI":"10.1145\/41457.37515","article-title":"Exploiting virtual synchrony in distributed systems","volume-title":"Proceedings of the eleventh ACM Symposium on Operating systems principles","author":"Birman","year":"1987"},{"key":"B8","first-page":"41","article-title":"A ros 2 response-time analysis exploiting starvation freedom and execution-time variance","volume-title":"IEEE real-time systems symposium RTSS","author":"Bla\u00df","year":"2021"},{"key":"B9","doi-asserted-by":"crossref","DOI":"10.1109\/IROS45743.2020.9341085","volume-title":"Verification of system-wide safety properties of ros applications","author":"Carvalho","year":"2020"},{"key":"B10","first-page":"1","article-title":"Response-time analysis of ros 2 processing chains under reservation-based scheduling","volume-title":"31st euromicro conference on real-time systems","author":"Casini","year":"2019"},{"key":"B11","doi-asserted-by":"publisher","first-page":"104301","DOI":"10.1016\/j.robot.2022.104301","article-title":"A formal toolchain for offline and run-time verification of robotic systems","volume":"159","author":"Dal Zilio","year":"2023","journal-title":"Robot. Aut. Syst."},{"key":"B12","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/3643663.3643970","article-title":"A model-based methodology for automated verification of ros 2 systems","volume-title":"Proceedings of the 2024 ACM\/IEEE 6th international workshop on robotics software engineering","author":"Dust","year":"2024"},{"key":"B13","first-page":"57","article-title":"Pattern-based verification of ros 2 nodes using uppaal","volume-title":"International conference on formal methods for industrial critical systems","author":"Dust","year":""},{"key":"B14","volume-title":"A model-based approach to automation of formal verification of ROS 2-based systems \u2014 sites.google.com","author":"Dust","year":"2025"},{"key":"B15","doi-asserted-by":"crossref","DOI":"10.1109\/ETFA54631.2023.10275668","article-title":"Experimental evaluation of callback behavior in ros 2 executors","volume-title":"28th international conf. On emerging technologies and factory automation","author":"Dust","year":""},{"key":"B16","unstructured":"Acceleo: code generator for eclipse"},{"key":"B17","unstructured":"Qvt operational mappings (qvto)"},{"key":"B18","unstructured":"Object management group\n          \n          \n            \n              Group\n              O. M.\n            \n          \n          \n          2022"},{"key":"B19","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1809.02595","article-title":"Towards a distributed and real-time framework for robots: Evaluation of ROS 2.0 communications for real-time robotic applications","author":"Guti\u00e9errez","year":"2018"},{"key":"B20","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1109\/FormaliSE.2017.9","article-title":"Formal verification of ros-based robotic applications using timed-automata","volume-title":"2017 IEEE\/ACM 5th international FME workshop on formal methods in software engineering (FormaliSE)","author":"Halder","year":"2017"},{"key":"B21","doi-asserted-by":"crossref","DOI":"10.1109\/QEST.2006.59","article-title":"Uppaal 4.0","volume-title":"Third international conference on the quantitative evaluation of systems - (QEST\u201906)","author":"Hendriks","year":"2006"},{"key":"B22","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1145\/3540250.3549164","article-title":"Robofuzz: fuzzing robotic systems over robot operating system (ros) for finding correctness bugs","volume-title":"Proceedings of the 30th ACM joint European software engineering conference and symposium on the foundations of software engineering","author":"Kim","year":"2022"},{"key":"B23","doi-asserted-by":"publisher","first-page":"102341","DOI":"10.1016\/j.sysarc.2021.102341","article-title":"Autoware_perf: a tracing and performance analysis framework for ros 2 applications","volume":"123","author":"Li","year":"2022","journal-title":"J. Syst. Archit."},{"key":"B24","doi-asserted-by":"crossref","DOI":"10.1109\/MEMCOD.2018.8556970","article-title":"Formal analysis and verification of dds in ros2","volume-title":"2018 16th ACM\/IEEE international conference on formal methods and models for system design (MEMOCODE)","author":"Liu","year":"2018"},{"key":"B25","unstructured":"Ros 2: documentation"},{"key":"B26","unstructured":"Ros: distributions"},{"key":"B27","doi-asserted-by":"crossref","DOI":"10.1109\/RoSE52553.2021.00012","article-title":"Specifying qos requirements and capabilities for component-based robot software","volume-title":"2021 IEEE\/ACM 3rd international workshop on robotics software engineering (RoSE)","author":"Parra","year":"2021"},{"key":"B28","doi-asserted-by":"crossref","first-page":"731","DOI":"10.1145\/1837274.1837461","article-title":"Cyber-physical systems: the next computing revolution","volume-title":"Proceedings of the 47th design automation conference","author":"Rajkumar","year":"2010"},{"key":"B29","unstructured":"Ros 2 realtime reference system"},{"key":"B30","unstructured":"Autoware reference system"},{"key":"B31","volume-title":"EMF: eclipse modeling framework","author":"Steinberg","year":"2008"},{"key":"B32","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1109\/RTSS55097.2022.00015","article-title":"End-to-end timing analysis in ros2","volume-title":"2022 IEEE real-time systems symposium (RTSS)","author":"Teper","year":"2022"},{"key":"B33","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1109\/thms.2015.2425139","article-title":"Toward reliable autonomous robotic assistants through formal verification: a case study","volume":"46","author":"Webster","year":"2016","journal-title":"IEEE Trans. Human-Machine Syst."}],"container-title":["Frontiers in Robotics and AI"],"original-title":[],"link":[{"URL":"https:\/\/www.frontiersin.org\/articles\/10.3389\/frobt.2025.1592523\/full","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T12:28:12Z","timestamp":1752668892000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.frontiersin.org\/articles\/10.3389\/frobt.2025.1592523\/full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,16]]},"references-count":33,"alternative-id":["10.3389\/frobt.2025.1592523"],"URL":"https:\/\/doi.org\/10.3389\/frobt.2025.1592523","relation":{},"ISSN":["2296-9144"],"issn-type":[{"value":"2296-9144","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,7,16]]},"article-number":"1592523"}}