Erik Ramsgaard Wognsen will defend his thesis:
"Batteries in Space:Designing Energy-Optimal Satellites with Statistical Model Checking", on Friday 26th of February 2016, 13:00, in room 0.2.13 at Selma Lagerlöfs Vej 300
Satellites provide humanity with many useful services such as communication, navigation, and observation of Earth and space. But for the services to work reliably, satellites must be carefully designed, programmed and verified. Formal methods provide many techniques to analyze, check, prove, and synthesize systems. But in addition to correctness we are also interested in energy and how it is used. This thesis follows the transition of formal methods research into quantitative territory.
Energy is scarce in space, so to get the most out of the satellites we have spent large sums to place in orbit, we must also understand how they use energy. We treat three topics, starting with batteries. We show that precise modeling of battery behavior in the context of formal methods enables more efficient operation without extensive safety margins, and that battery-aware scheduling can reduce energy waste. On the other hand, pushing a battery to the limit to provide optimal short term performance reduces long term battery life over hundreds of recharge cycles.
We provide a method to evaluate the long term effect of proposed usage profiles on the battery and weigh them against the benefit of the increased short term performance.
The second topic concerns the actual energy use in satellite equipment such as radio transceivers.
Many electronic circuits and computations can be expressed as dataflow graphs. First we show how a translation of dataflow graphs to priced timed automata enables the use of cost-optimal reachability algorithms to perform energy-optimal scheduling, and how this can be used to study trade-offs between time and energy. For the specific dataflow formalism finite-state machine-based scenario-aware dataflow, we develop a systematic translation to timed automata such that general properties of the dataflow graphs can be model checked.
The final topic is the correct operation of computer processors in space. We formalize a realistic low-level assembly language and show how programs in it can be modified to guarantee detection of computation errors caused by transient bit errors in data registers, thus making satellite software more resilient to high-energy particles found outside our atmosphere as well as aggressive power saving techniques.
Members of the assessment committee
Professor Jan Madsen, Technical University of Denmark, Professor Paul Petterson, Mälardalen University and Associate Professor Bent Thomsen, Aalborg University. Professor Kim Guldstrand and Associate Professor René Rydhof Hansen are Erik Ramsgaard Wognsen's supervisors. Moderator Associate Professor Jiri Srba.
All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.