研究目的
To propose and evaluate an automated verification method using software model checking to formally verify the design of stand-alone solar photovoltaic systems, ensuring the intended behavior before deployment.
研究成果
The automated verification method using software model checking effectively identifies sizing errors and details conditions leading to failures in stand-alone solar PV systems, which are not detected by simulation tools. The method provides a reliable approach to validate PV system designs before deployment, ensuring intended behavior. Future work includes expanding case studies, developing a general-purpose simulation tool for comparison, and extending the method to other types of renewable energy systems.
研究不足
1. Model precision: The mathematical models used for PV system components may not capture all real-world complexities.
2. Time step: The algorithm uses a one-hour time step, which may not fully approximate real-world scenarios.
3. Case studies: The study is limited to case studies in one municipality, potentially limiting the generalizability of the results.
4. Simulation Tool: Only HOMER Pro was used for comparison; other tools might yield different results.
5. Temperature and Solar Irradiance Data: Data used are from the closest municipality, not from the exact locations of the case studies.
1：Experimental Design and Method Selection:
The study employs automated verification using model checking to validate the design of stand-alone solar photovoltaic systems. The methodology includes mathematical modeling of each component of the system and the use of three state-of-the-art model checkers (CBMC, ESBMC, CPAchecker) to verify the system's design against user requirements.
2：Sample Selection and Data Sources:
Five case studies of stand-alone solar PV systems were selected, ranging from 253 W to 814 W. Data sources include manufacturer's data for PV components and load curves estimated from surveys.
3：List of Experimental Equipment and Materials:
The study involves PV panels, batteries, charge controllers, and inverters as part of the stand-alone solar PV systems.
4：Experimental Procedures and Operational Workflow:
The verification process involves writing PV input data and mathematical models in ANSI-C code, performing a sizing check, and then using model checkers to verify the system's design. The process includes exploring weather variables systematically and checking for property violations.
5：Data Analysis Methods:
The results from automated verification and simulation tools (HOMER Pro) were compared with real-world data collected from the deployed systems to validate the approach.
独家科研数据包，助您复现前沿成果，加速创新突破
获取完整内容
