Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids (Artifact)

In our paper titled "Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids", presented at the 2021 NASA Formal Methods Symposium, we study a smart grid with wind power and battery storage. Traditionally, day-ahead planning aims to balance demand and wind power, yet actual wind conditions often deviate from forecasts. Short-term flexibility in storage and generation fills potential gaps, planned on a minutes time scale for 30-60 minute horizons. Finding the optimal flexibility deployment requires solving a semi-infinite non-convex stochastic program, which is generally intractable to do exactly. Previous approaches rely on sampling, yet such critical problems call for rigorous approaches with stronger guarantees. Our method employs probabilistic model checking techniques. First, we cast the problem as a continuous-space Markov decision process with discretized control, for which an optimal deployment strategy minimizes the expected grid frequency deviation. To mitigate state space explosion, we exploit specific structural properties of the model to implement an iterative exploration method that reuses pre-computed values as wind data is updated. This artifact contains all code and data needed to reproduce the results presented in the paper. Instructions on how to install and use the code are included in the ReadMe.txt file in the artifact.

本研究发表于2021年美国国家航空航天局（NASA）形式化方法研讨会（NASA Formal Methods Symposium），论文题为《风电与储能协同优化：面向智能电网的预测性验证》，针对集成风电与储能系统的智能电网开展研究。传统日前规划旨在实现用电需求与风电出力的平衡，但实际风电工况往往与预测结果存在偏差。储能与发电的短时灵活性调节可填补潜在缺口，这类调节以分钟级时间尺度进行规划，覆盖30至60分钟的预测时域。寻求最优灵活性调度方案需要求解半无限非凸随机规划问题，而精确求解此类问题通常难以实现。现有方法多依赖采样策略，但这类关键问题亟需具备更强可靠性保证的严谨求解方法。本研究提出的方法采用概率模型检验（probabilistic model checking）技术。首先，我们将该问题建模为带有离散化控制的连续空间马尔可夫决策过程（Markov Decision Process, MDP），其最优调度策略可最小化电网频率偏差的期望值。为缓解状态空间爆炸问题，我们利用模型的特定结构特性，设计了一种迭代探索方法：当风电数据更新时，该方法可复用预计算得到的数值结果。本附属资源包包含复现论文中所有结果所需的全部代码与数据，代码的安装与使用说明已收录于该资源包内的ReadMe.txt文件中。