Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 10:05 - 10:30 at Sainte-Catherine - Session 1 Chair(s): Matteo Rossi

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 fixed-points 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.

Mon 27 May

Displayed time zone: Eastern Time (US & Canada) change

08:40 - 10:30
Session 1FormaliSE at Sainte-Catherine
Chair(s): Matteo Rossi Politecnico di Milano
08:40
10m
Day opening
Welcome by the Chairs
FormaliSE
C: Stefania Gnesi Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
08:50
25m
Full-paper
Epistemic Model Checking of Distributed Commit Protocols with Byzantine faults
FormaliSE
Omar Bataineh NTU, Mark Reynolds The Univeristy of Western Australia
09:15
25m
Full-paper
Clock Reduction in Timed Automata while Preserving Design Parameters
FormaliSE
Beyazit Yalcinkaya Middle East Technical University, Ebru Aydin Gol Middle East Technical University
09:40
25m
Full-paper
Rigorous Design and Deployment of IoT Applications
FormaliSE
Ajay Krishna Inria Grenoble, France, Michel Le Pallec Nokia Bell Labs, Radu Mateescu INRIA, Ludovic Noirie Nokia Bell Labs, Gwen Salaün University of Grenoble Alpes
10:05
25m
Full-paper
Static Analysis for Worst-Case Battery Utilization
FormaliSE