Using Statistical Model Checking for Power Scheduling in Nanosatellites

Abstract:

Nanosatellites are miniature satellites, typically lighter than 10 kg. Their primary power source is solar energy but the small size limits solar panel area and space for energy storage. The windows for harvesting solar energy depend on the orbit of the satellite which in turn depends on its mission. Satellite subsystems have different energy and real-time demands -- some can be shut down, others cannot, and some have hard real-time constraints. In my work I aim to use statistical model checking to study energy scheduling and optimization in nanosatellites. Model checking is a well-known verification technique and the statistical features are useful for modeling stochasticity and for simulating loads combined with realistic battery models described as hybrid systems. Stochastic behavior includes the (energy required by the) payload of the satellite, transient errors caused by cosmic ray impacts, and energy harvesting variation due to inaccuracies in attitude control.