Battery-aware scheduling in low orbit: the GomX–3 case
- 47 Downloads
When working with space systems the keyword is resources. For a satellite in orbit all resources are scarce and the most critical resource of all is power. It is therefore crucial to have detailed knowledge on how much power is available for an energy harvesting satellite in orbit at every time—especially when in eclipse, where it draws its power from onboard batteries. The challenge is to maximise operational performance of a satellite, while providing hard guarantees that critically low battery levels are avoided, taking into account these power restrictions. Classic approaches to workload scheduling and analysis are not suitable, because of heterogeneity, interdependencies and system dynamics involved. This paper addresses this problem by a two-step procedure to perform task scheduling for low-earth-orbit satellites exploiting formal methods. It combines time-bounded cost-optimal reachability analyses of priced timed automata networks with a realistic kinetic battery model capable of capturing capacity limits as well as stochastic fluctuations. We also discuss how the time-bounded analysis can be embedded into a workflow that exploits in-orbit current and voltage measurements so as to perpetuate the task scheduling. The core procedure has been exercised in-orbit for the automatic and resource-optimal day-ahead scheduling of GomX–3, a power-hungry 3-unit nanosatellite. We explain how this approach has overcome existing problems, has led to improved designs, and has provided new insights.
KeywordsBattery-aware scheduling Model predictive control Kinetic battery model State of charge estimation Kalman filter Nanosatellite
Unable to display preview. Download preview PDF.
This work has received support from the EU 7th Framework Programme Project 318490 (SENSATION), by the European Space Agency under contract number RFP/NC/IPL-PTE/GLC/as/881.2014, by the ERC Advanced Investigators Grant 695614 (POWVER), and by the CDZ Project 1023 (CAP). We are grateful to Boudewijn Haverkort and Marijn Jongerden (both from Universiteit Twente), Kim Larsen, Marius Mikučonis, Erik Ramsgaard Wognsen (all from Aalborg University), and all further participants of SENSATION as well as experts at GomSpace for very fruitful discussion and support.
- AB95.Agn JC, Bensana E (1995) Exact and approximate methods for the daily management of an earth observation satelliteGoogle Scholar
- BFH+01.Behrmann G, Fehnker A, Hune T, Larsen KG, Pettersson P, Romijn J, Vaandrager FW (2001) Minimum-cost reachability for priced timed automata. In: Di Benedetto MD, Sangiovanni-Vincentelli AL (eds) Hybrid systems: computation and control, 4th international workshop, HSCC 2001, Rome, Italy, March 28–30, 2001, proceedings, volume 2034 of lecture notes in computer science. Springer, pp 147–161Google Scholar
- BGH+16.Bisgaard M, Gerhardt D, Hermanns H, Krcál J, Nies G, Stenger M (2016) Battery-aware scheduling in low orbit: The gomx-3 case. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM 2016: formal methods—21st international symposium, Limassol, Cyprus, November 9–11, 2016, proceedings, volume 9995 of lecture notes in computer science, pp 559–576Google Scholar
- FGD+11.Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) Spaceex: Scalable verification of hybrid systems. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification-23rd international conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011, proceedings, volume 6806 of lecture notes in computer science. Springer, pp 379–395Google Scholar
- HH16.Hahn EM, Hartmanns A (2016) A comparison of time- and reward-bounded probabilistic model checking techniques. In: Fränzle M, Kapur D, Zhan N (eds) Dependable software engineering: theories, tools, and applications-2nd international symposium, SETTA, Beijing, China, November 9–11, 2016, proceedings, volume 9984 of lecture notes in computer science. pp 85–100Google Scholar
- HKN17.Hermanns H, Krčál J, Nies G (2017) How is your satellite doing? Battery kinetics with recharging and uncertainty. Leibniz Trans Embed Syst 4(1): 04–10428Google Scholar
- HPP99.Harrison SA, Price ME, Philpott MS (1999) Task scheduling for satellite based imagery. In: Proceedings of the eighteenth workshop of the UK planning and scheduling special interest group, volume 78. University of Sanford, UK, pp 64–78Google Scholar
- Inc16.Texas Instruments Incorporated (2016) Tms570 active cell-balancing battery-management design guideGoogle Scholar
- Jon10.Jongerden MR (2010) Model-based energy analysis of battery powered systems. Ph.D. Thesis, Enschede, December 2010Google Scholar
- LBB+01.Larsen K, Behrmann G, Brinksma E, Fehnker A, Hune T, Pettersson P, Romijn J (2001) As cheap as possible: Effcient cost-optimal reachability for priced timed automata. In: Computer aided verification. Springer, pp 493–505Google Scholar
- Ple02.Plett GL (2002) Kalman-filter soc estimation for lipb hev cells. In: Proceedings of the 19th international battery, hybrid and fuel cell electric vehicle symposium and exhibition (EVS19). Busan, Korea, pp 527–538Google Scholar
- SÁMK17.Schupp S, Ábrahám E, Makhlouf IB, Kowalewski S (2017) Hypro: a C++ library of state set representations for hybrid systems reachability analysis. In: Barrett C, Davies M, Kahsai T (eds) NASA formal methods-9th international symposium, NFM 2017, Moffett Field, CA, USA, May 16–18, 2017, proceedings, volume 10227 of lecture notes in computer science, pp 288–294Google Scholar
- ST15.Sebastiani R, Trentin P (2015) Optimathsat: a tool for optimization modulo theories. In: Kroening D, Pasareanu CS (eds) Computer aided verification-27th international conference, CAV, San Francisco, CA, USA, July 18–24, 2015, proceedings, Part I, volume 9206 of lecture notes in computer science. Springer, pp 447–454Google Scholar
- upp05.Uppaal Cora (2005) http://people.cs.aau.dk/~adavid/cora/introduction.html
- WHL14.Wognsen ER, Hansen RR, Larsen KG (2014) Battery-aware scheduling of mixed criticality systems. In: International symposium on leveraging applications of formal methods, verification and validation. Springer, pp 208–222Google Scholar
- ZNL+17.Zhang Z, Nielsen B, Larsen KG, Nies G, Stenger M, Hermanns H (2017) Pareto optimal reachability analysis for simple priced timed automata. In: Duan Z, Ong L (eds) Formal methods and software engineering—19th international conference on formal engineering methods, ICFEM, Xi’an, China, November 13–17, proceedings, volume 10610 of lecture notes in computer science. Springer, pp 481–495Google Scholar