Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management

TL;DR

This paper explores how detailed battery features impact the formal verification of autonomous robots, using a UAV inspection case and discussing integration of battery health management for improved safety and reliability.

Contribution

It models battery behavior in formal verification of autonomous robots and discusses integrating battery health management to enhance safety verification.

Findings

Battery features significantly influence verification outcomes.

Dynamic environments and safety strategies jointly affect robot safety.

Probabilistic model checking reveals critical battery-related risks.

Abstract

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.