TY - GEN
T1 - Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management
AU - Zhao, Xingyu
AU - Osborne, Matthew
AU - Lantair, Jennifer
AU - Robu, Valentin
AU - Flynn, David
AU - Huang, Xiaowei
AU - Fisher, Michael
AU - Papacchini, Fabio
AU - Ferrando, Angelo
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
KW - Autonomous systems
KW - Battery PHM
KW - Formal verification
KW - PRISM
KW - Probabilistic model checking
KW - Unmanned aerial vehicle
UR - http://www.scopus.com/inward/record.url?scp=85072872810&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-30446-1_6
DO - 10.1007/978-3-030-30446-1_6
M3 - Conference contribution
SN - 9783030304454
T3 - Lecture Notes in Computer Science
SP - 105
EP - 124
BT - Software Engineering and Formal Methods
A2 - Ölveczky, Peter Csaba
A2 - Salaün, Gwen
PB - Springer
T2 - 17th International Conference on Software Engineering and Formal Methods 2019
Y2 - 16 September 2019 through 20 September 2019
ER -