- The test setup described in Ernits et al. [9] uses UPPAAL Tron [10] as the primary test execution engine. First, the QA team should model, in UPPAAL, (i) an implementation model of the system under test and (ii) a topological map of the environment. Second, the QA team integrates an adapter, provided by Ernits et al. [9], which is responsible for translating messages between the environment model and the appropriate topics in ROS, acting as the interface between the ROS-based system under test and the UPPAAL Tron model of the environment. Finally, the interaction between the implementation model (i) and the environment model (ii) is monitored during system execution and afterwards, the equivalence between the measured outcomes from the running system and the outcomes from the model is checked. The operating environment, however, is typically prone to uncertainty which makes modeling the environment a costly activity. + The test setup described in Ernits et al. [9] uses UPPAAL Tron [10] as the primary test execution engine. First, the QA team should model, in UPPAAL, (i) an implementation model of the system under test and (ii) a topological map of the environment. Second, the QA team integrates an adapter, provided by Ernits et al. [9], which is responsible for translating messages between the environment model and the appropriate topics in ROS, acting as the interface between the ROS-based system under test and the UPPAAL Tron model of the environment. Finally, the interaction between the implementation model (i) and the environment model (ii) is monitored during system execution and afterwards, the equivalence between the measured outcomes from the running system and the outcomes from the model is checked. The operating environment, however, is typically prone to uncertainty which makes modeling the environment a costly activity. +
+ ++ Building on the use of UPPAAL for ROS verification, Dust et al. [13, 14] propose a pattern-based approach with reusable timed automata templates that model the execution behavior of ROS 2 nodes, including callback scheduling, buffer overflow, and end-to-end latency in processing chains. The approach supports both single-threaded and multi-threaded executors and has been validated against real ROS 2 execution traces. A model-based methodology further automates the process [15]: system parameters are extracted from ROS 2 execution traces generated by the ROS2_tracing tool, then transformed through Eclipse Ecore metamodels into initialized UPPAAL formal model templates via model-to-model and model-to-text transformations, reducing the manual effort and domain expertise previously required for formal model construction.
[10] K. G. Larsen, M. Mikucionis et al., “Testing real-time embedded software using uppaal-tron: an industrial case study,” in Proceedings of the 5th ACM international conference on Embedded software, 2005, pp. 299–306.
[11] N. Hammoudeh Garcia, M. L¨udtke et al., “Bootstrapping mde development from ros manual code - part 1: Metamodeling,” in 2019 Third IEEE International Conference on Robotic Computing (IRC), 2019, pp. 329–336.
[12] N. Hammoudeh Garc´ıa, H. Deshpande et al., “Bootstrapping mde development from ros manual code: Part 2—model generation and leveraging models at runtime,” Software and Systems Modeling, vol. 20, no. 6, pp. 2047–2070, 2021.
+[13] L. Dust, R. Gu, C. Seceleanu, M. Ekström, and S. Mubeen, “Pattern-Based Verification of ROS 2 Nodes Using UPPAAL,” in Formal Methods for Industrial Critical Systems (FMICS), Lecture Notes in Computer Science, vol. 14290, Springer, 2023, pp. 57–75.
+[14] L. Dust, R. Gu, C. Seceleanu, M. Ekström, and S. Mubeen, “Pattern-based verification of ROS 2 applications using UPPAAL,” International Journal on Software Tools for Technology Transfer (STTT), vol. 27, pp. 313–332, 2025.
+[15] L. Dust, R. Gu, S. Mubeen, M. Ekström, and C. Seceleanu, “A model-based approach to automation of formal verification of ROS 2-based systems,” Frontiers in Robotics and AI, vol. 12, 2025.
diff --git a/index.html b/index.html index 86e7d83..954e9d1 100644 --- a/index.html +++ b/index.html @@ -149,9 +149,9 @@Guidelines for Developers and QA Teams
What's New
+
- March 2026 — New exemplar added: UPPAAL automated verification toolchain for ROS 2 timing and scheduling analysis (PE2).
- March 2026 — New contribution templates: you can now suggest tools, report gaps, or request updates directly via GitHub Issues — no Git required.
- March 2026 — Website refresh: updated contact info, copyright, and contribution guidelines.
-- July 2024 — Initial release of the guideline catalog accompanying the TSE paper.