モジュール式ロボットシステムの合成検証に向けて
Towards Compositional Verification for Modular Robotic Systems
モジュール式ロボットの各コンポーネントを異なる検証手法で個別に検証しつつ、一階述語論理の契約で前提と保証を記述して全体の整合性を合成的に検証する手法を提案し、遠隔検査ロボットの例で示した論文。
著者: Rafael C. Cardoso, Louise A. Dennis, Marie Farrell, Michael Fisher, Matt Luckcuck
分類: cs.SE, cs.LO, cs.RO
原文アブストラクト
Software engineering of modular robotic systems is a challenging task, however, verifying that the developed components all behave as they should individually and as a whole presents its own unique set of challenges. In particular, distinct components in a modular robotic system often require different verification techniques to ensure that they behave as expected. Ensuring whole system consistency when individual components are verified using a variety of techniques and formalisms is difficult. This paper discusses how to use compositional verification to integrate the various verification techniques that are applied to modular robotic software, using a First-Order Logic (FOL) contract that captures each component's assumptions and guarantees. These contracts can then be used to guide the verification of the individual components, be it by testing or the use of a formal method. We provide an illustrative example of an autonomous robot used in remote inspection. We also discuss a way of defining confidence for the verification associated with each component.
