Résumé
Energy intermittency in solar-powered embedded systems threatens Quality of Service (QoS) and system autonomy. In this study, we address the design of these systems with a formal co-design approach that provides verifiable guarantees, a critical advantage over traditional heuristic or predictive methods that often fail under unpredictable conditions. We use timed automatabased modeling within Uppaal Stratego to minimize grid reliance and battery capacity in a typical system, under QoS guarantees. Our methodology demonstrates that synthesized control strategies can reduce grid reliance by 58-72%, while an optimized task scheduling heuristic can decrease required battery capacity by up to 13% compared to the baseline. Our approach provides a formal basis for comparing these techniques to inform system design.