研究目的
提出并评估一种使用软件模型检测的自动化验证方法，以形式化验证独立太阳能光伏系统的设计，确保在部署前实现预期行为。
研究成果
这种利用软件模型检测的自动化验证方法能有效识别独立光伏系统中的容量配置错误，并详细呈现导致系统故障的条件——这些是仿真工具无法检测到的。该方法为光伏系统设计部署前的验证提供了可靠途径，确保系统按预期运行。未来工作包括扩展案例研究、开发通用仿真工具进行对比分析，以及将该方法推广至其他类型可再生能源系统。
研究不足
1. 模型精度：用于光伏系统组件的数学模型可能无法涵盖现实中的所有复杂因素。 2. 时间步长：该算法采用一小时为时间步长，可能无法完全模拟现实场景。 3. 案例研究：本研究仅限于一个城市的案例，可能影响结果的普适性。 4. 仿真工具：仅使用HOMER Pro进行对比，其他工具可能产生不同结果。 5. 温度与太阳辐照数据：所用数据来自最近的城市，而非案例研究的确切位置。
1：实验设计与方法选择：
本研究采用基于模型检测的自动化验证技术来验证独立太阳能光伏系统的设计。该方法包括对系统各组件进行数学建模，并使用三种先进的模型检测器（CBMC、ESBMC、CPAchecker）根据用户需求验证系统设计。
2：样本选择与数据来源：
选取了5个功率范围在253瓦至814瓦之间的独立太阳能光伏系统案例。数据来源包括光伏组件的制造商数据和通过调查估算的负载曲线。
3：实验设备与材料清单：
研究涉及的独立太阳能光伏系统组件包括光伏板、蓄电池、充电控制器和逆变器。
4：实验流程与操作步骤：
验证过程包括用ANSI-C代码编写光伏输入数据和数学模型，进行容量校核，然后使用模型检测器验证系统设计。该流程包括系统性地探索天气变量并检查属性违规情况。
5：数据分析方法：
将自动化验证和仿真工具（HOMER Pro）的结果与实际部署系统收集的真实数据进行对比，以验证该方法的有效性。
独家科研数据包，助您复现前沿成果，加速创新突破
获取完整内容-
PV Panels
325 W
Convert solar energy into DC electricity
-
Batteries
220 Ah
Store energy for use during night or rainy days
-
Charge Controller
150 V/35 A
Manage energy flow to PV system, batteries, and loads
-
Inverter
700 W
Convert DC to AC for AC loads
-
HOMER Pro
v3.12.0
Simulation tool for renewable energy systems
-
ESBMC
v6.0.0
Bounded model checker for C programs
-
CBMC
5.11
C Bounded Model Checker
-
CPAchecker
1.8
Configurable Program Analysis Checker
-
登录查看剩余6件设备及参数对照表
查看全部
