AS2FM：为鲁棒自主性启用ROS 2系统的统计模型检验
机器人学
2025-08-27 v1 形式语言与自动机理论
摘要
设计能在不可预见环境中自主行动的机器人系统是一项具有挑战性的任务。本工作提出了一种新颖的方法，在设计时使用形式化验证，特别是统计模型检验（SMC），来验证自主机器人的系统属性。我们引入了SCXML格式的扩展，旨在对包括机器人操作系统2（ROS 2）和行为树（BT）特性在内的系统组件进行建模。此外，我们贡献了自主系统到形式化模型（AS2FM）工具，用于将完整的系统模型转换为JANI。使用JANI这种定量模型检验的标准格式，能够利用现成的SMC工具验证系统属性。我们展示了AS2FM的实际可用性，既体现在对真实世界自主机器人控制系统的适用性上，也体现在验证运行时的可扩展性上。我们提供了一个案例研究，其中我们成功识别了一个基于ROS 2的机器人操作用例中的问题，该用例可在消费级硬件上于不到一秒内完成验证。此外，我们与现有技术进行了比较，证明我们的方法在系统特性支持方面更全面，并且验证运行时随模型大小呈线性增长，而非指数增长。
引用
@article{arxiv.2508.18820,
title = {AS2FM: Enabling Statistical Model Checking of ROS 2 Systems for Robust Autonomy},
author = {Christian Henkel and Marco Lampacrescia and Michaela Klauck and Matteo Morelli},
journal= {arXiv preprint arXiv:2508.18820},
year = {2025}
}
备注
Accepted at IROS2025