バッテリー健全性管理を組み込んだ自律ロボットの形式検証に向けて
Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management
風力発電所を点検するUAVのミッションをPRISMで確率モデル検査し、バッテリーの容量劣化や放電特性が検証結果に大きく影響することを示した論文。
著者: Xingyu Zhao, Matt Osborne, Jenny Lantair, Valentin Robu, David Flynn, Xiaowei Huang, Michael Fisher, Fabio Papacchini, Angelo Ferrando
分類: cs.AI, cs.RO, cs.SY, eess.SP, eess.SY
原文アブストラクト
The battery is a key component of autonomous robots. Its performance limits the robot's safety and reliability. Unlike liquid-fuel, a battery, as a chemical device, exhibits complicated features, including (i) capacity fade over successive recharges and (ii) increasing discharge rate as the state of charge (SOC) goes down for a given power demand. Existing formal verification studies of autonomous robots, when considering energy constraints, formalise the energy component in a generic manner such that the battery features are overlooked. In this paper, we model an unmanned aerial vehicle (UAV) inspection mission on a wind farm and via probabilistic model checking in PRISM show (i) how the battery features may affect the verification results significantly in practical cases; and (ii) how the battery features, together with dynamic environments and battery safety strategies, jointly affect the verification results. Potential solutions to explicitly integrate battery prognostics and health management (PHM) with formal verification of autonomous robots are also discussed to motivate future work.
