Designing a Tool-Chain For Generating Battery-Aware Contact Plans Using UPPAAL
Translated title
Design af en toolchain til generation af batteri-opmærksomme kontakt planer ved brug af UPPAAL
Authors
Degn, Kristoffer Mathiasen ; Kørvell, August Malling
Term
4. term
Education
Publication year
2019
Abstract
This thesis examines how UPPAAL can be used to schedule data delivery in the Ulloriaq mission’s constellation of micro LEO satellites, where limited battery resources and the lack of persistent end-to-end links make planning challenging. We cast the problem as a delay-tolerant network and develop a toolchain that generates and then verifies battery-aware contact plans (schedules of when satellites can communicate). The constellation is first modeled as a network of Priced Timed Automata with a simple linear battery model and a store-carry-forward scheme; UPPAAL CORA is used to find a cost-optimal run that meets goals for fast, energy-conscious delivery. A custom extractor turns this run into a concrete contact plan. To capture more realistic battery behavior, a Stochastic Timed Automata model based on KiBaM with uncertainty in loads and initial charge is then applied, and UPPAAL SMC estimates the probability of battery depletion to verify the plan. The toolchain can turn raw orbital data into verified contact plans, though some manual setup is still required. Across experiments varying heuristics and mission parameters, confidence in the models increased, and comparison with prior MILP-based work showed that, while plans were not identical, their overall behavior was similar.
Denne afhandling undersøger, hvordan UPPAAL kan bruges til at planlægge dataoverførsel i Ulloriaq-missionens konstellation af mikro LEO-satellitter, hvor begrænsede batterier og manglende vedvarende end-to-end-forbindelser gør planlægning vanskelig. Vi formulerer problemet som et forsinkelsestolerant netværk og udvikler en værktøjskæde, der genererer og efterfølgende verificerer batteribevidste kontaktplaner (planer for, hvornår satellitter kan kommunikere). Først modelleres konstellationen som et netværk af Priced Timed Automata med en enkel lineær batterimodel og en store-carry-forward-strategi; UPPAAL CORA bruges til at finde en omkostningsoptimal kørsel, der opfylder målet om hurtig og energibevidst levering. En skræddersyet extractor omdanner derefter denne kørsel til en konkret kontaktplan. For at afspejle mere realistisk batteriadfærd anvendes dernæst en Stochastic Timed Automata-model baseret på KiBaM med usikkerheder i belastninger og initial ladning, og UPPAAL SMC estimerer risikoen for batteritømning for at verificere planen. Værktøjskæden kan ud fra rå bane-data producere verificerede kontaktplaner, men processen kræver endnu noget manuel opsætning. Gennem flere eksperimenter med heuristikker og missionsparametre øgedes tilliden til modellen, og en sammenligning med tidligere MILP-baserede resultater viste, at de genererede planer ikke var identiske, men havde tilsvarende overordnet adfærd.
[This apstract has been generated with the help of AI directly from the project full text]