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

Zhao, Xingyu ORCID: 0000-0002-3474-349X, Osborne, Matt, Lantair, Jenny, Robu, Valentin, Flynn, David, Huang, Xiaowei ORCID: 0000-0001-6267-0366, Fisher, Michael, Papacchini, Fabio ORCID: 0000-0002-0310-7378 and Ferrando, Angelo ORCID: 0000-0002-8711-4670 (2019) Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management. .

Text
1909.03019v1.pdf - Author Accepted Manuscript
Download (1MB) | Preview

Official URL: http://dx.doi.org/10.1007/978-3-030-30446-1_6

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.

Item Type:	Conference or Workshop Item (Unspecified)
Uncontrolled Keywords:	Formal verification, Probabilistic model checking, PRISM, Autonomous systems, Unmanned aerial vehicle, Battery PHM
Depositing User:	Symplectic Admin
Date Deposited:	17 Sep 2019 08:04
Last Modified:	19 Jan 2023 00:26
DOI:	10.1007/978-3-030-30446-1_6
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3054808