{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:28Z","timestamp":1779087568272,"version":"3.51.4"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["695614"],"award-info":[{"award-number":["695614"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000844","name":"European Space Agency","doi-asserted-by":"publisher","award":["RFP\/NC\/IPL- PTE\/GLC\/as\/881.2014"],"award-info":[{"award-number":["RFP\/NC\/IPL- PTE\/GLC\/as\/881.2014"]}],"id":[{"id":"10.13039\/501100000844","id-type":"DOI","asserted-by":"publisher"}]},{"name":"European Union (FP7)","award":["318490"],"award-info":[{"award-number":["318490"]}]},{"name":"Chinesisch-Deutsches Zentrum f\u00fcr Wissenschaftsf\u00f6rderung","award":["1023"],"award-info":[{"award-number":["1023"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2019,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            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\u2014especially 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 G\n            <jats:sc>om<\/jats:sc>\n            X\u20133, 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.\n          <\/jats:p>","DOI":"10.1007\/s00165-018-0458-2","type":"journal-article","created":{"date-parts":[[2018,7,4]],"date-time":"2018-07-04T06:53:20Z","timestamp":1530687200000},"page":"261-285","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Battery-aware scheduling in low orbit: the GomX\u20133 case"],"prefix":"10.1145","volume":"31","author":[{"given":"Morten","family":"Bisgaard","sequence":"first","affiliation":[{"name":"GomSpace ApS, Aalborg, Denmark"}]},{"given":"David","family":"Gerhardt","sequence":"additional","affiliation":[{"name":"GomSpace ApS, Aalborg, Denmark"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Saarland University \u2013 Computer Science, Saarland Informatics Campus, Saarbr\u00fccken, Germany"}]},{"given":"Jan","family":"Kr\u010d\u00e1l","sequence":"additional","affiliation":[{"name":"Saarland University \u2013 Computer Science, Saarland Informatics Campus, Saarbr\u00fccken, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2535-1590","authenticated-orcid":false,"given":"Gilles","family":"Nies","sequence":"additional","affiliation":[{"name":"Saarland University \u2013 Computer Science, Saarland Informatics Campus, Saarbr\u00fccken, Germany"}]},{"given":"Marvin","family":"Stenger","sequence":"additional","affiliation":[{"name":"Saarland University \u2013 Computer Science, Saarland Informatics Campus, Saarbr\u00fccken, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Agn JC Bensana E (1995) Exact and approximate methods for the daily management of an earth observation satellite"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"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\u201330 2001 proceedings volume 2034 of lecture notes in computer science. Springer pp 147\u2013161","DOI":"10.1007\/3-540-45351-2_15"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bisgaard M Gerhardt D Hermanns H Krc\u00e1l 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\u201421st international symposium Limassol Cyprus November 9\u201311 2016 proceedings volume 9995 of lecture notes in computer science pp 559\u2013576","DOI":"10.1007\/978-3-319-48989-6_34"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1059816.1059823"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Frehse G Le Guernic C Donz\u00e9 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\u201320 2011 proceedings volume 6806 of lecture notes in computer science. Springer pp 379\u2013395","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Hahn EM Hartmanns A (2016) A comparison of time- and reward-bounded probabilistic model checking techniques. In: Fr\u00e4nzle M Kapur D Zhan N (eds) Dependable software engineering: theories tools and applications-2nd international symposium SETTA Beijing China November 9\u201311 2016 proceedings volume 9984 of lecture notes in computer science. pp 85\u2013100","DOI":"10.1007\/978-3-319-47677-3_6"},{"issue":"1","key":"e_1_2_1_2_8_2","first-page":"04","article-title":"How is your satellite doing? Battery kinetics with recharging and uncertainty","volume":"4","author":"Hermanns H","year":"2017","journal-title":"Leibniz Trans Embed Syst"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0377-2217(94)90385-9"},{"key":"e_1_2_1_2_10_2","unstructured":"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\u201378"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpowsour.2004.09.020"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TVT.2011.2132812"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apenergy.2011.08.002"},{"key":"e_1_2_1_2_14_2","unstructured":"Texas Instruments Incorporated (2016) Tms570 active cell-balancing battery-management design guide"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1049\/iet-sen.2009.0001"},{"key":"e_1_2_1_2_16_2","unstructured":"Jongerden MR (2010) Model-based energy analysis of battery powered systems. Ph.D. Thesis Enschede December 2010"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1115\/1.3662552"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"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\u2013505","DOI":"10.1007\/3-540-44585-4_47"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpowsour.2007.03.072"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/3220923.3221253"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0038-092X(93)90060-2"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1090\/dimacs\/057\/06","article-title":"A constraint-based approach to satellite scheduling","volume":"57","author":"Pemberton JC","year":"2001","journal-title":"DIMACS Ser Discrete Math Theor Comput Sci"},{"key":"e_1_2_1_2_24_2","unstructured":"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\u2013538"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0378-7753(01)00560-2"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Schupp S \u00c1brah\u00e1m 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\u201318 2017 proceedings volume 10227 of lecture notes in computer science pp 288\u2013294","DOI":"10.1007\/978-3-319-57288-8_20"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"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\u201324 2015 proceedings Part I volume 9206 of lecture notes in computer science. Springer pp 447\u2013454","DOI":"10.1007\/978-3-319-21690-4_27"},{"key":"e_1_2_1_2_28_2","unstructured":"U ppaal C ora (2005) http:\/\/people.cs.aau.dk\/~adavid\/cora\/introduction.html"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011203002719"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"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\u2013222","DOI":"10.1007\/978-3-662-45231-8_15"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"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\u201419th international conference on formal engineering methods ICFEM Xi\u2019an China November 13\u201317 proceedings volume 10610 of lecture notes in computer science. Springer pp 481\u2013495","DOI":"10.1007\/978-3-319-68690-5_29"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0458-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0458-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0458-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0458-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:58:04Z","timestamp":1641538684000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0458-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["10.1007\/s00165-018-0458-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0458-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4]]},"assertion":[{"value":"7 September 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 July 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}