宇宙ロボットのモジュール式検証手法
Modular Verification of Autonomous Space Robotics
各ノードの前提と保証を一階述語論理で記述し、テストや形式手法による個別検証を統合してシステム全体の信頼度を測る手法を提案した論文。
著者: Marie Farrell, Rafael C. Cardoso, Louise A. Dennis, Clare Dixon, Michael Fisher, Georgios Kourtis, Alexei Lisitsa, Matt Luckcuck, Matt Webster
分類: cs.SE, cs.RO
原文アブストラクト
Ensuring that autonomous space robot control software behaves as it should is crucial, particularly as software failure in space often equates to mission failure and could potentially endanger nearby astronauts and costly equipment. To minimise mission failure caused by software errors, we can utilise a variety of tools and techniques to verify that the software behaves as intended. In particular, distinct nodes in a robotic system often require different verification techniques to ensure that they behave as expected. This paper introduces a method for integrating the various verification techniques that are applied to robotic software, via a First-Order Logic (FOL) specification that captures each node's assumptions and guarantees. These FOL specifications are then used to guide the verification of the individual nodes, be it by testing or the use of a formal method. We also outline a way of measuring our confidence in the verification of the entire system in terms of the verification techniques used.
