AI 中文总结
该研究针对数据中心电压穿越控制器设计难题，提出SolVRT系统，用形式化方法合成合规控制器，通过仿真验证其可生成合规控制器、诊断不可行性并识别针对性修改。
AI 中文摘要
数据中心是电网中增长最快的负荷之一。由于数据中心服务器是敏感的电子元件，需要在电网故障期间保护其免受电网电压扰动的影响。虽然从电网断开连接可以实现这一点，但如果许多数据中心同时跳闸，可能会进一步破坏电力系统的稳定性。为解决这一新兴问题，电压穿越（VRT）电网规范已被提出，以规范数据中心的行为。这些规范要求数据中心在扰动期间保持连接一段时间，维持有功功率下限，并在电网恢复后的截止期限内恢复其功率消耗。然而，系统设计和验证满足这些耦合的时间和运行要求的控制器仍然具有挑战性。我们提出了SolVRT，这是一个使用形式化方法为给定数据中心合成符合电网规范的VRT控制器的系统。我们开发了一种规范语言，将电网规范表示为信号时序逻辑（STL），作为形式化推理的基础。我们的编码算法接受该规范以及数据中心电力拓扑的模型，并将约束转化为控制器合成问题。如果找到解决方案，此步骤将生成一个构造正确的控制器；若未找到解决方案，则生成不存在此类控制器的证明。对于后一种情况，SolVRT提供诊断步骤：追踪设施的“冲突前沿”，分离导致不符合要求的冲突条款，并计算最小的硬件或工作负载变更以实现合规。我们通过对连接到140节点输电系统的200 MW数据中心进行闭环仿真来评估SolVRT。结果表明，SolVRT可以合成符合要求的VRT控制器，在无法实现合规时验证其不可行性，并识别使合规成为可能的针对性修改。
英文摘要
Data centers are among the power grid's fastest-growing loads. Since data center servers are sensitive electronic components, they need to be protected against the grid's voltage disturbances during grid faults. While disconnecting from the grid achieves this, it can further destabilize the power system if many data centers trip at once. To address this emerging concern, voltage ride-through (VRT) grid codes have been proposed to standardize data center behavior. They require a data center to stay connected for a period of time through the disturbance, hold an active power floor, and recover its draw within a deadline upon restoration. However, systematically designing and certifying controllers that satisfy these coupled temporal and operational requirements remains challenging. We propose SolVRT, a system that synthesizes a grid-code-compliant VRT controller for a given data center using formal methods. We develop a specification language that expresses a grid code in Signal Temporal Logic (STL) as the basis for formal reasoning. Our encoding algorithm takes the specification, along with a model of the data center's power topology, and translates the constraints into a controller synthesis problem. This step produces a correct-by-construction controller if a solution can be found, or a proof that no such controller exists. For the latter case, SolVRT provides a diagnostic step: it traces the facility's "conflict frontier," isolates the conflicting clauses that led to non-compliance, and computes the smallest hardware or workload change that would enable compliance. We evaluate SolVRT through closed-loop simulations of a 200 MW data center connected to a 140-bus transmission system. The results demonstrate that SolVRT can synthesize compliant VRT controllers, certify infeasibility when compliance is unattainable, and identify targeted modifications that enable compliance.
Comments12 pages, 10 figures, 1 table
