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

Xingyu Zhao, Matthew Osborne, Jennifer Lantair, Valentin Robu, David Flynn, Xiaowei Huang, Michael Fisher, Fabio Papacchini, Angelo Ferrando

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods
Subtitle of host publicationSEFM 2019
EditorsPeter Csaba Ölveczky, Gwen Salaün
PublisherSpringer
Pages105-124
Number of pages20
ISBN (Electronic)9783030304461
ISBN (Print)9783030304454
DOIs
Publication statusPublished - 2019
Event17th International Conference on Software Engineering and Formal Methods 2019 - Oslo, Norway
Duration: 16 Sep 201920 Sep 2019

Publication series

NameLecture Notes in Computer Science
Volume11724
ISSN (Print)0302-9743

Conference

Conference17th International Conference on Software Engineering and Formal Methods 2019
Abbreviated titleSEFM 2019
CountryNorway
CityOslo
Period16/09/1920/09/19

Fingerprint

Health
Robots
Liquid fuels
Model checking
Unmanned aerial vehicles (UAV)
Farms
Inspection
Formal verification
Statistical Models

Keywords

  • Autonomous systems
  • Battery PHM
  • Formal verification
  • PRISM
  • Probabilistic model checking
  • Unmanned aerial vehicle

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Zhao, X., Osborne, M., Lantair, J., Robu, V., Flynn, D., Huang, X., ... Ferrando, A. (2019). Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management. In P. C. Ölveczky, & G. Salaün (Eds.), Software Engineering and Formal Methods: SEFM 2019 (pp. 105-124). (Lecture Notes in Computer Science; Vol. 11724). Springer. https://doi.org/10.1007/978-3-030-30446-1_6
Zhao, Xingyu ; Osborne, Matthew ; Lantair, Jennifer ; Robu, Valentin ; Flynn, David ; Huang, Xiaowei ; Fisher, Michael ; Papacchini, Fabio ; Ferrando, Angelo. / Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management. Software Engineering and Formal Methods: SEFM 2019. editor / Peter Csaba Ölveczky ; Gwen Salaün. Springer, 2019. pp. 105-124 (Lecture Notes in Computer Science).
@inproceedings{0380614d06194c019149c06e44cb333d,
title = "Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management",
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.",
keywords = "Autonomous systems, Battery PHM, Formal verification, PRISM, Probabilistic model checking, Unmanned aerial vehicle",
author = "Xingyu Zhao and Matthew Osborne and Jennifer Lantair and Valentin Robu and David Flynn and Xiaowei Huang and Michael Fisher and Fabio Papacchini and Angelo Ferrando",
year = "2019",
doi = "10.1007/978-3-030-30446-1_6",
language = "English",
isbn = "9783030304454",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "105--124",
editor = "{\"O}lveczky, {Peter Csaba} and Gwen Sala{\"u}n",
booktitle = "Software Engineering and Formal Methods",

}

Zhao, X, Osborne, M, Lantair, J, Robu, V, Flynn, D, Huang, X, Fisher, M, Papacchini, F & Ferrando, A 2019, Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management. in PC Ölveczky & G Salaün (eds), Software Engineering and Formal Methods: SEFM 2019. Lecture Notes in Computer Science, vol. 11724, Springer, pp. 105-124, 17th International Conference on Software Engineering and Formal Methods 2019, Oslo, Norway, 16/09/19. https://doi.org/10.1007/978-3-030-30446-1_6

Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management. / Zhao, Xingyu; Osborne, Matthew; Lantair, Jennifer; Robu, Valentin; Flynn, David; Huang, Xiaowei; Fisher, Michael; Papacchini, Fabio; Ferrando, Angelo.

Software Engineering and Formal Methods: SEFM 2019. ed. / Peter Csaba Ölveczky; Gwen Salaün. Springer, 2019. p. 105-124 (Lecture Notes in Computer Science; Vol. 11724).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

ER -

Zhao X, Osborne M, Lantair J, Robu V, Flynn D, Huang X et al. Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management. In Ölveczky PC, Salaün G, editors, Software Engineering and Formal Methods: SEFM 2019. Springer. 2019. p. 105-124. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-30446-1_6