Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management
This work addresses safety and reliability issues for autonomous robots, particularly in domains like UAVs, by highlighting the need to integrate battery prognostics into verification, but it is incremental as it builds on existing formal verification methods.
The paper tackles the problem of formal verification for autonomous robots by showing that overlooking detailed battery features like capacity fade and discharge rate can significantly affect verification results, as demonstrated through a UAV inspection case study using probabilistic model checking in PRISM.
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.