Submitted: February 2018


What makes scheduling of real-time systems in space so difficult are resources or rather the shortage thereof, particularly when dealing with space systems like CubeSats. These are miniaturised satellites used for space research, e. g. testing of new space technologies. CubeSats are, on the one hand, very resource-hungry and, on the other hand, provide only little room for components like batteries, solar panels, and other payloads. They harvest energy via photovoltaic modules and store it in an on-board battery to maintain service even when they enter eclipse.

This thesis presents a fully automated routine for battery-aware task scheduling of the nanosatellite GomX-3. The satellite is modelled as a network of timed automata extended with rewards in the modelling language Modest. Schedules are obtained via reward-optimal reachability analysis performed by the model checker and simulator of the Modest Toolset.