Automated formal verification of stand-alone solar photovoltaic systems.

• Verification can be effective to validate stand-alone solar photovoltaic systems. • Automated verification method can detect design errors better than simulation. • ESBMC can produce better performance and soundness among automated verifiers. With declining costs and increasing performance, the deployment of renewable energy systems is growing faster. In 2017, for the first time, the number of people without access to electricity dropped down below 1 billion, but trends on energy access likewise fall short of global goals. Particular attention is given to stand-alone solar photovoltaic systems in rural areas or where grid extension is unfeasible. Tools to evaluate electrification projects are available, but they are based on simulations that do not cover all aspects of the design-space. Automated verification using model checking has proven to be an effective technique to validate complex (state transition) systems. This paper marks the first application of software model checking to formally verify the design of a stand-alone solar photovoltaic system, including solar panel, charge controller, battery, inverter, and electric load. Our main focus is on the project validation to be carried out just after the system sizing, i.e., prior to buying equipment and deployment, as a safe approach to ensure the intended behavior. Five case studies were used to evaluate this proposed approach and to compare that with specialized simulation tool. Different verification tools were evaluated to compare performance and soundness among automated verifiers. The results reported by our automated verification method and by the simulation tool were compared with data collected from dwellers of the deployed cases, thereby showing the effectiveness of our approach, where specific conditions that lead to failures in a solar photovoltaic system are only detailed by the automated verification method. [ABSTRACT FROM AUTHOR]