AS2FM: ROS 2システムの統計的モデル検査による堅牢な自律性の実現
AS2FM: Enabling Statistical Model Checking of ROS 2 Systems for Robust Autonomy
ROS 2とビヘイビアツリーをSCXML拡張でモデル化し、JANI形式に変換して統計的モデル検査を行うツールAS2FMを提案。ロボットマニピュレーションのケーススタディで問題を1秒未満で検出し、検証時間がモデルサイズに対して線形にスケールすることを示した。
詳しい要約
1. どんなもの？
2. 先行研究と比べてどこがすごい？
3. 技術・手法の肝は？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
※ AIが要旨から生成した要約です。正確性は原文をご確認ください。
著者: Christian Henkel, Marco Lampacrescia, Michaela Klauck, Matteo Morelli
分類: cs.RO, cs.FL
原文アブストラクト
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.
