一种验证模块化机器人系统的组合性方法

《Robotics and Autonomous Systems》：A compositional approach to verifying modular robotic systems

　　

介绍了ROS合同语言（ROS Contract Language）以及解析/监控合成工具Vanda；简单、基于一阶逻辑（FOL）的合同；从合同自动合成形式化运行时监控（Runtime Monitors）；适用于机器人操作系统（ROS）程序，可扩展至非ROS系统；使用异质性验证方法（Heterogeneous verification methods）验证实现是否符合合同。

**论文解读：一种验证模块化机器人系统的组合性方法**

**研究背景与问题**
机器人系统在工业安全关键场景中日益普及，如海上结构监测、核检查与退役、空间探索等。控制机器人的软件工程复杂，常依赖模块化框架（如ROS或GenoM）。确保软件行为正确性至关重要，尤其随着系统自主性增强、复杂性提升，且与人类共享动态环境。然而，机器人软件框架的通用性与灵活性使正确性保证极具挑战。现有形式化方法包括模型检验、运行时验证、定理证明等，但不同方法间结果关联困难。研究人员此前指出，机器人领域需整合形式化与非形式化验证方法。Assume–Guarantee推理（或前置/后置条件）是成熟的组合性验证技术，通过合同（contract）分解系统为模块，各自独立验证。但合同需与实际需求一致。

**研究内容与结论**
本文提出一种针对ROS系统的组合性验证方法，聚焦于研究问题：能否用组合性、异质性方法验证基于ROS的系统？方法包括：手动抽象ROS程序为系统模型，为每个节点编写基于一阶逻辑（FOL）的Assume–Guarantee合同，利用演算推理节点组合并推导系统级属性，使用异质性验证方法确认节点实现，并自动合成运行时监控（Runtime Monitors）作为安全网。工具链包括ROS合同语言（RCL）和原型工具Vanda。通过远程检查火星车案例研究（基于Gazebo仿真）验证方法有效性。结论：该方法能有效引入形式化规范到现有ROS系统，支持组合性、异质性验证，并自动生成低开销运行时监控。论文发表在《Robotics and Autonomous Systems》。

**关键技术方法**（不超过250字）
研究人员用到以下关键技术：1）**ROS合同语言（RCL）**：一种领域特定语言（DSL），基于一阶逻辑（FOL）编写Assume–Guarantee合同，链接ROS主题与变量。2）**合同演算**：包含序列、分支、合并规则（R1-R4），使用一阶时序逻辑（FOTL）的“next”（○）和“eventually”（?）算子推导系统级属性。3）**异质性验证**：结合模型检查（AJPF）、定理证明（Dafny、Hoare Logic）、代码审查、实验测试等方法，验证各节点满足合同。4）**运行时监控合成**：通过Vanda工具自动从RCL合同生成RML（Runtime Monitoring Language）规范，并集成ROSMonitoring框架生成监控节点。案例研究无样本队列，所有验证基于仿真环境。

**研究结果**

**Step 1: Creating a system model**
通过手动分析ROS图（rqt_graph），将远程检查火星车系统抽象为四个复合节点：Localisation（定位）、Navigation（导航）、Agent（智能体）、Radiation Sensor（辐射传感器）。去除或合并了可靠库节点（如move base），并添加外部节点（Agent）。

**Step 2: Specifying node contracts**
为每个节点编写RCL合同，定义输入输出、假设与保证。例如，Agent节点合同包含三个保证：移动至下一航点、检查未检查点、遇到危险辐射时返回出口。通过映射规则（Scalar、Collection、Function）将ROS主题变量与合同变量关联。

**Step 3: Deriving system-level properties**
应用演算规则R3（输入合并）推导系统级属性：若Localisation和Radiation Sensor的保证蕴含Agent的假设，则当机器人处于有效唯一位置且辐射正常时，Agent的保证最终成立。该属性支持四个系统需求（REQ1-4）。

**Step 4a: Heterogeneous verification**
- **Localisation节点**：通过代码审查验证其输出唯一位置（?!x,y∈R·Position(x,y)），因仿真无噪声。
- **Navigation节点**：通过47次实验测试，平均定位误差21.4 cm（标准差4 mm），在预设25 cm容忍度内，满足合同。
- **Agent节点**：使用AJPF模型检查器验证Gwendolen BDI程序，将合同保证映射为LTL属性（如`□(B_jackal_going(4)??B_jackal_going(5))`），验证所有12个航点及安全返回逻辑。
- **Radiation Sensor节点**：使用Hoare Logic手工证明，验证输入辐射值分类为绿色（<120）、橙色（120-250）、红色（≥250）及检查标志为真。

**Step 4b: Automatic synthesis of runtime monitors**
Vanda自动从RCL合同生成RML规范及ROSMonitoring配置。例如，Agent节点的RML包含事件类型与保证项（如`command(inspect,i)`）。监控器在运行时订阅主题（如Snapshot），线性时间开销可忽略（平均约0%额外时间）。

**讨论与结论**
讨论部分指出方法支持节点互换性（如用Dafny替代Gwendolen实现Agent，验证合同一致性），并展示可应用于非ROS系统（如Simulink模型）。结论翻译：本文贡献了一种开发可验证模块化机器人系统的组合性方法，聚焦于ROS系统（部分适用于非ROS）。每个模块（或ROS节点）用FOL的Assume–Guarantee合同指定，指导验证。提出演算组合合同，支持序列、连接和分支。每个节点可用最合适方法验证，合同驱动验证。作为安全网，自动合成形式化监控验证运行时保证。远程检查案例研究（第4节）为现有系统指定合同，使用形式化与非形式化验证技术。方法优势在于合同引导验证，即使节点规范语言不直接实现FOL也有效。未来工作包括扩展RCL处理服务与动作、规模化验证、自动化演算等。