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

## TL;DR

This paper introduces a model-based toolchain to automate formal verification of ROS 2 systems, making safety checks easier and more efficient for robotics developers.

## Contribution

The novel contribution is a model-driven methodology that automates formal verification of ROS 2 systems using execution traces and UPPAAL models.

## Key findings

- The toolchain automates parameter extraction and model generation from ROS 2 execution traces.
- Experiments on implemented and conceptual systems validate the toolchain's correctness and adaptability.
- The methodology supports both individual node and end-to-end latency verification in ROS 2 systems.

## Abstract

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.