Formal Modeling and Analysis of Small-Scale Data Centers Integrating Renewable Energy Using Timed Automata

Integrating renewable energy into data centers is essential for reducing reliance on fossil fuels and minimize the environmental impact of digital infrastructures. However, the variability and unpredictability of renewable sources come with significant design and operational challenges. This paper introduces a formal modeling framework for solar-powered small-scale data centers, using stochastic timed automata and statistical model checking for mathematical analysis. The solution supports efficient resource sizing, reduces grid energy consumption through optimized workload scheduling and server renewal strategies. It enables robustness evaluation under component failure scenarios. A case study demonstrates the applicability, flexibility, and scalability of the framework for distributed system topologies and energy-aware design exploration.