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

17 Downloads (Pure)

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

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