Automated Formal Verification of Stand-alone Solar Photovoltaic Systems

Alessandro Bezerra Trindade, Lucas Cordeiro

Research output: Contribution to journalArticlepeer-review

151 Downloads (Pure)


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.
Original languageEnglish
JournalSolar Energy
Early online date15 Oct 2019
Publication statusPublished - 2019


  • Formal verification
  • model checking
  • photovoltaic power systems


Dive into the research topics of 'Automated Formal Verification of Stand-alone Solar Photovoltaic Systems'. Together they form a unique fingerprint.

Cite this