How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty

Holger Hermanns, Jan Krčál, Gilles Nies


The kinetic battery model is a popular model of the dynamic behaviour of a conventional battery, useful to predict or optimize the time until battery depletion. The model however lacks certain obvious aspects of batteries in-the-wild, especially with respect to the effects of random influences and the behaviour when charging up to capacity limits.

This paper considers the kinetic battery model with limited capacity in the context of piecewise constant yet random charging and discharging. We provide exact representations of the battery behaviour wherever possible, and otherwise develop safe approximations that bound the probability distribution of the battery state from above and below. The resulting model enables the time-dependent evaluation of the risk of battery depletion. This is demonstrated in an extensive dependability study of a nano satellite currently orbiting the earth. 


Battery Power; Depletion Risk; Bounded Charging and Discharging; Stochastic Load; Distribution Bounds

Full Text:



Alessandro Abate, Maria Prandini, John Lygeros, and Shankar Sastry. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica, 44(11):2724-2734, 2008. URL:

European Space Agency.ESA Cubesat program, October 2014. URL:

Eitan Altman and Vladimir Gaitsgory. Asymptotic optimization of a nonlinear hybrid system governed by a markov decision process. SIAM Journal on Control and Optimization, 35(6):2070-2085, 1997. URL:

Henk A. P. Blom and John Lygeros, editors. Stochastic Hybrid systems: Ttheory and Safety Critical Applications, volume 337 of Lecture Notes in Control and Information Science. Springer Heidelberg, 2006. URL:

Udi Boker, Thomas A. Henzinger, and Arjun Radhakrishna. Battery transition systems. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'14, San Diego, CA, USA, January 20-21, 2014, pages 595-606. ACM, 2014. URL:

M. Brandl, H. Gall, M. Wenger, V. Lorentz, M. Giegerich, Federico Baronti, Gabriele Fantechi, Luca Fanucci, Roberto Roncella, Roberto Saletti, Sergio Saponara, Alexander Thaler, Martin Cifrain, and W. Prochazka. Batteries and battery management systems for electric vehicles. In Wolfgang Rosenstiel and Lothar Thiele, editors, 2012 Design, Automation & Test in Europe Conference & Exhibition, DATE 2012, Dresden, Germany, March 12-16, 2012, pages 971-976. IEEE, 2012. URL:

Isidor Buchmann. Batteries in a portable world. Cadex Electronics Richmond, 2001.

Manuela L. Bujorianu, John Lygeros, and Marius C. Bujorianu. Bisimulation for general stochastic hybrid systems. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005, Proceedings, volume 3414 of Lecture Notes in Computer Science, pages 198-214. Springer, 2005. URL:

J. Cao, N. Schofield, and A. Emadi. Battery balancing methods: A comprehensive review. In Vehicle Power and Propulsion Conference, 2008. VPPC'08. IEEE, pages 1-6, Sept 2008. URL:

Lucia Cloth, Marijn R. Jongerden, and Boudewijn R. Haverkort. Computing battery lifetime distributions. In The 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2007, 25-28 June 2007, Edinburgh, UK, Proceedings, pages 780-789. IEEE Computer Society, 2007. URL:

Robert M. Corless, Gaston H. Gonnet, D. E. G. Hare, David J. Jeffrey, and Donald E. Knuth.On the LambertW function. Adv. Comput. Math., 5(1):329-359, 1996. URL:

Mark H. A. Davis. Piecewise-deterministic markov processes: A general class of non-diffusion stochastic models. Journal of the Royal Statistical Society. Series B (Methodological), pages 353-388, 1984. URL:

Marc Doyle, Thomas F. Fuller, and John Newman. Modeling of galvanostatic charge and discharge of the lithium/polymer/insertion cell. Journal of The Electrochemical Society, 140(6):1526-1533, 1993. URL:

Maria Fox, Derek Long, and Daniele Magazzeni. Automatic construction of efficient multiple battery usage policies. In Toby Walsh, editor, IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 2620-2625. IJCAI/AAAI, 2011. URL:

Martin Fränzle. Personal communication. 2015.

Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick, and Lijun Zhang. Measurability and safety verification for stochastic hybrid systems. In Marco Caccamo, Emilio Frazzoli, and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pages 43-52. ACM, 2011. URL:

Martin Fränzle, Holger Hermanns, and Tino Teige. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Workshop, HSCC 2008, St. Louis, MO, USA, April 22-24, 2008. Proceedings, volume 4981 of Lecture Notes in Computer Science, pages 172-186. Springer, 2008. URL:

Pascal Gilles. Private communication. 2014.

Daniel T. Gillespie. A general method for numerically simulating the stochastic time evolution of coupled chemical reactions. Journal of Computational Physics, 22(4):403-434, 1976. URL:

GomSpace. Gomspace gomx-1, October 2014. URL:

Thomas A. Henzinger. Verification of Digital and Hybrid Systems, chapter The Theory of Hybrid Automata, pages 265-292. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000. URL:

Holger Hermanns, Jan Krcál, and Gilles Nies. Recharging probably keeps batteries alive. In Christian Berger and Mohammad Reza Mousavi, editors, Cyber Physical Systems. Design, Modeling, and Evaluation - 5th International Workshop, CyPhy 2015, Amsterdam, The Netherlands, October 8, 2015, Proceedings, volume 9361 of Lecture Notes in Computer Science, pages 83-98. Springer, 2015. URL:

Marijn R. Jongerden and Boudewijn R. Haverkort. Which battery model to use?IET Software, 3(6):445-457, 2009. URL:

Marijn R. Jongerden, Boudewijn R. Haverkort, Henrik C. Bohnenkamp, and Joost-Pieter Katoen. Maximizing system lifetime by battery scheduling. In Proceedings of the 2009 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2009, Estoril, Lisbon, Portugal, June 29 - July 2, 2009, pages 63-72. IEEE Computer Society, 2009. URL:

Marijn Remco Jongerden. Model-based energy analysis of battery powered systems. PhD thesis, University of Twente, Enschede, December 2010. URL:

Edward A. Lee and David G. Messerschmitt. Synchronous data flow. Proceedings of the IEEE, 75(9):1235-1245, 1987. URL:

Bor Yann Liaw, E. Peter Roth, Rudolph G. Jungst, Ganesan Nagasubramanian, Herbert L. Case, and Daniel H. Doughty. Correlation of arrhenius behaviors in power and capacity fades with cell impedance and heat generation in cylindrical lithium-ion cells. Journal of power sources, 119:874-886, 2003. URL:

James F. Manwell and Jon G. McGowan. Lead acid battery storage model for hybrid energy systems. Solar Energy, 50(5):399-405, 1993. URL:

John Newman. Fortran programs for the simulation of electrochemical systems. URL:

Wilhelm Peukert.Über die Abhängigkeit der Kapazität von der Entladestromstärke bei Bleiakkumulatoren. Elektrotechnische Zeitschrift, 20:20-21, 1897.

Daler N. Rakhmatov and Sarma B. K. Vrudhula. An analytical high-level battery model for use in energy management of portable electronic systems. In Rolf Ernst, editor, Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2001, San Jose, CA, USA, November 4-8, 2001, pages 488-493. IEEE Computer Society, 2001. URL:

Venkatasailanathan Ramadesigan, Paul W. C. Northrop, Sumitava De, Shriram Santhanagopalan, Richard D. Braatz, and Venkat R. Subramanian. Modeling and simulation of lithium-ion batteries from a systems engineering perspective. Journal of The Electrochemical Society, 159(3):R31-R45, 2012. URL:

Venkat Rao, Gaurav Singhal, Anshul Kumar, and Nicolas Navet. Battery model for embedded systems. In 18th International Conference on VLSI Design (VLSI Design 2005), with the 4th International Conference on Embedded Systems Design, 3-7 January 2005, Kolkata, India, pages 105-110. IEEE Computer Society, 2005. URL:

Robin A. Sahner and Kishor S. Trivedi. Performance and reliability analysis using directed acyclic graphs.IEEE Trans. Software Eng., 13(10):1105-1114, 1987. URL:

Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. Probabilistic reach-avoid computation for partially degenerate stochastic processes.IEEE Trans. Automat. Contr., 59(2):528-534, 2014. URL:

Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts, and Alessandro Abate. Faust^2: Formal abstractions of uncountable-state stochastic processes. CoRR, abs/1403.3286, 2014. URL:

Jeremy Sproston. Decidable model checking of probabilistic hybrid automata. In Mathai Joseph, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium, FTRTFT 2000, Pune, India, September 20-22, 2000, Proceedings, volume 1926 of Lecture Notes in Computer Science, pages 31-45. Springer, 2000. URL:

Bart D. Theelen, Marc Geilen, Twan Basten, Jeroen Voeten, Stefan Valentin Gheorghita, and Sander Stuijk. A scenario-aware data flow model for combined long-run average and worst-case performance analysis. In 4th ACM&IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2006), 27-29 July 2006, Embassy Suites, Napa, California, USA, pages 185-194. IEEE Computer Society, 2006. URL:

Bart D. Theelen, Marc C. W. Geilen, Sander Stuijk, Stefan V. Gheorghita, Twan Basten, Jeroen P. M. Voeten, and Amir H. Ghamarian. Scenario-aware dataflow. Technical report, Eindhoven University of Technology, 2008. Technical Report ESR-2008-08. URL:

Manuel Villén-Altamirano and José Villén-Altamirano. Restart: a straightforward method for fast simulation of rare events. In Deborah A. Sadowski, Andrew F. Seila, Mani S. Manivannan, and Jeffrey D. Tew, editors, Proceedings of the 26th conference on Winter simulation, WSC 1994, Lake Buena Vista, FL, USA, December 11-14, 1994, pages 282-289. ACM, 1994. URL:

Kai Wang, Florin Ciucu, Chuang Lin, and Steven H. Low. A stochastic power network calculus for integrating renewable energy sources into the power grid.IEEE Journal on Selected Areas in Communications, 30(6):1037-1048, 2012. URL:

Erik Ramsgaard Wognsen, René Rydhof Hansen, and Kim Guldstrand Larsen. Battery-aware scheduling of mixed criticality systems. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part II, volume 8803 of Lecture Notes in Computer Science, pages 208-222. Springer, 2014. URL:

Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, and Ernst Moritz Hahn. Safety verification for probabilistic hybrid systems. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 196-211. Springer, 2010. URL:



Copyright (c) 2016 Holger Hermanns, Jan Krčál, Gilles Nies

Creative Commons License CC BY
This work is licensed under a Creative Commons Attribution 3.0 Germany License (CC BY 3.0 DE).

License URL:

Published by the European Design and Automation Association (EDAA) \ EMbedded Systems Special Interest Group (EMSIG) and Schloss Dagstuhl -- Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing.