A model-based approach to automation of formal verification of ROS 2-based systems

Area of Science:

• Robotics
• Formal Methods
• Software Engineering

Background:

• Formal verification is crucial for ensuring the correctness and safety of robotic applications, especially those using ROS 2.
• Current methods face challenges due to complexity and manual effort in model creation and parameter extraction.

Purpose of the Study:

• To propose a model-based methodology and toolchain for automating the formal verification of ROS 2 systems.
• To enhance the adoption of formal methods by reducing manual effort and complexity.

Main Methods:

• A model-driven engineering approach using a toolchain to automate formal model initialization in UPPAAL.
• Utilizing ROS 2 execution traces (via ROS2_tracing) for system parameter derivation.
• Employing four Ecore metamodel-based representations for structural and verification aspects.
• Supporting iterative verification via model-to-model and model-to-text transformations.

Main Results:

• A proof-of-concept implementation demonstrated the feasibility of the automated toolchain.
• The toolchain supports verification of individual ROS 2 nodes (e.g., callback latency) and end-to-end processing chains.
• Experiments on implemented and conceptual ROS 2 systems validated the toolchain's correctness and adaptability.

Conclusions:

• The proposed methodology automates parameter extraction and model generation for formal verification of ROS 2 systems.
• It modularizes the verification process, enhancing traceability and reusability for robotics developers.
• The approach makes formal verification more accessible and practical for the robotics community.