Publisher DOI: 10.1109/FormaliSE.2019.00009
Title: Static Analysis for Worst-Case Battery Utilization
Language: English
Authors: Ivanov, Dmitry 
Schupp, Sibylle 
Keywords: battery utilization;fixed-point computation for total lattices;KiBaM;static analysis;worklist algorithm
Issue Date: May-2019
Source: IEEE/ACM 7th International Workshop on Formal Methods in Software Engineering, FormaliSE 2019 : 8807517 (2019-05)
Abstract (english): 
Lithium-ion batteries demonstrate two kinds of nonlinear behavior: rate capacity effects and recovery effects. These effects are dual to each other and show the dependency between the power consumption profile and battery utilization, i.e., the fraction of the battery charge that can be withdrawn.We propose a static analysis for computing the lower bound of battery utilization based on the Kinetic Battery Model (KiBaM), an analytical model capturing nonlinear battery behavior. Our method does not depend on the battery charge level and can be composed with other flow analyses and model checking techniques for improved accuracy. We propose a modification to the worklist algorithm for totally ordered semilattices with computable fixedpoints of transfer functions, which is necessary for computing our analysis. We prove the termination and correctness of our algorithm and introduce a nonforgetful extension to it for speeding up convergence. We implement the battery-utilization in the software verification tool CPAchecker by encoding the analysis together with our algorithm in a relaxed instance of a configurable program analysis (CPA). Our experiments show that the convergence speed up is sometimes achievable, but does not necessarily lead to a performance improvement.
Conference: IEEE/ACM 7th International Workshop on Formal Methods in Software Engineering, FormaliSE 2019 
ISBN: 978-172813373-7
Institute: Softwaresysteme E-16 
Document Type: Chapter/Article (Proceedings)
Appears in Collections:Publications without fulltext

Show full item record

Page view(s)

Last Week
Last month
checked on Sep 24, 2021

Google ScholarTM


Add Files to Item

Note about this record

Cite this record


Items in TORE are protected by copyright, with all rights reserved, unless otherwise indicated.