用统计模型检测验证机器人系统，1秒内完成验证
AS2FM: Enabling Statistical Model Checking of ROS 2 Systems for Robust Autonomy
- 扩展SCXML格式，融合ROS 2与行为树建模
- 在消费级硬件上1秒内完成机器人操作验证
- 适合机器人系统设计阶段的可靠性验证
在未知环境中实现机器人自主运行是极具挑战的任务。本文提出一种基于形式化验证的全新方法，采用统计模型检查（SMC）在设计阶段验证自主机器人的系统属性。我们扩展了SCXML格式，用于建模包含ROS 2和行为树（BT）特性的系统组件，并开发了AS2FM工具，将完整系统模型转换为标准的JANI格式。利用JANI这一量化模型检查通用格式，可借助现成的SMC工具验证系统性质。我们在实际机器人控制系统中验证了AS2FM的可用性，结果显示其验证时间可线性随模型规模增长，而非指数增长，且在消费级硬件上对一个基于ROS 2的机器人操作案例的验证耗时不足1秒。与现有技术相比，本方法支持更全面的系统特性，且验证效率显著提升。
原文摘要 · Abstract (English)
Designing robotic systems to act autonomously in unforeseen environments is a challenging task. This work presents a novel approach to use formal verification, specifically Statistical Model Checking (SMC), to verify system properties of autonomous robots at design-time. We introduce an extension of the SCXML format, designed to model system components including both Robot Operating System 2 (ROS 2) and Behavior Tree (BT) features. Further, we contribute Autonomous Systems to Formal Models (AS2FM), a tool to translate the full system model into JANI. The use of JANI, a standard format for quantitative model checking, enables verification of system properties with off-the-shelf SMC tools. We demonstrate the practical usability of AS2FM both in terms of applicability to real-world autonomous robotic control systems, and in terms of verification runtime scaling. We provide a case study, where we successfully identify problems in a ROS 2-based robotic manipulation use case that is verifiable in less than one second using consumer hardware. Additionally, we compare to the state of the art and demonstrate that our method is more comprehensive in system feature support, and that the verification runtime scales linearly with the size of the model, instead of exponentially.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。