为ROS 2发布订阅机制提供形式化建模与验证框架
Formal Modeling and Verification of Publisher-Subscriber Paradigm in ROS 2
- 用时序自动机网络形式化描述ROS 2发布订阅行为
- 证明模型与实际执行路径完全一致，确保分析可靠性
- 适合安全关键型机器人系统开发者与形式化验证研究者
机器人操作系统（ROS）是开发机器人应用最流行的中间件，但在安全关键环境中用于实时系统时存在显著缺陷。为此，ROS 2于2017年发布，旨在支持分布式机器人系统的实时能力，同时保留原版ROS的核心特性。然而，针对ROS程序的形式化保证与正确性研究仍不充分。本文提出一个框架，以解决保障机器人系统正确行为这一挑战性问题。我们构建了ROS 2程序的形式化模型，并用时序自动机网络描述其行为。证明该模型与时序自动机网络的执行集合完全一致。因此，分析ROS 2发布订阅场景时，算法首先将程序转换为模型，再转化为时序自动机网络。通过在简化系统和实际机器人系统上进行实验，验证了方法的有效性与适用性，并讨论了结果与局限。
原文摘要 · Abstract (English)
The Robot Operating System (ROS) is one of the most popular middleware for developing robot applications, but it is subject to major shortcomings when applied to real-time robotic systems in safety-critical environments. For this reason, ROS 2 was released in 2017 for implementing real-time capabilities in distributed robotic systems while supporting the most prominent aspects of the original ROS. There is still not much work done to provide formal guarantees and correctness of a ROS program. In this paper, we propose a framework to address this challenging problem of guaranteeing the correct behaviour of robotic systems. We propose a formal modelling of a ROS 2 program, and also describe the program using a network of timed automata. We then prove that the sets of executions of a ROS program in the model and in the network of timed automata are the same. Thus to analyze a publisher-subscriber scenario of ROS 2 program, our algorithm first converts the program into the model, and then into the network of timed automata. The applicability and validity of our approach are verified by conducting several experiments on a simplified system and an actual robotic system, and the results and limitations are discussed.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。