Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation
With decreasing costs and increasing performance, the deployment of renewable energy systems is now growing faster than in the past decade. In 2017, for the first time, the number of people without access to electricity dipped below 1 billion, but trends in energy access still fall short of global g...
| Autor principal: | Trindade, Alessandro Bezerra |
|---|---|
| Outros Autores: | http://lattes.cnpq.br/4511445991061477, https://orcid.org/0000-0001-8262-2919 |
| Grau: | Tese |
| Idioma: | eng |
| Publicado em: |
Universidade Federal do Amazonas
2020
|
| Assuntos: | |
| Acesso em linha: |
https://tede.ufam.edu.br/handle/tede/7671 |
| id |
oai:https:--tede.ufam.edu.br-handle-:tede-7671 |
|---|---|
| recordtype |
dspace |
| spelling |
oai:https:--tede.ufam.edu.br-handle-:tede-76712020-02-18T05:03:42Z Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation Verificação Automática de Sistemas Solares Fotovoltaicos Off-grid: Dimensionamento Ótimo e Validação de Projeto Trindade, Alessandro Bezerra Cordeiro, Lucas Carvalho http://lattes.cnpq.br/4511445991061477 http://lattes.cnpq.br/5005832876603012 Mota, Edjard de Souza http://lattes.cnpq.br/0757666181169076 Barreto, Raimundo da Silva http://lattes.cnpq.br/1132672107627968 Silva, Sidelmo Magalhães http://lattes.cnpq.br/4356279128408928 https://orcid.org/0000-0001-8262-2919 Sistema solar fotovoltaico Energia renovável Verificação formal Verificação automatizada Sistemas de energia elétrica CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO Formal verification Automated verification Model checking Program synthesis Electrical systems Solar photovoltaic systems With decreasing costs and increasing performance, the deployment of renewable energy systems is now growing faster than in the past decade. In 2017, for the first time, the number of people without access to electricity dipped below 1 billion, but trends in energy access still 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 or to size electrification projects are available, but they are based on simulations that do not cover all aspects of the design space. However, the use of formal methods to model and validate any system has grown with time, mainly to find bugs in sophisticated hardware and software systems: they aim to establish system correctness with mathematical rigor. The use of formal methods in electrical systems is a new subject, with published research spanning only the last four years. Moreover, the use of automated synthesis in order to obtain optimal sizing of solar photovoltaic systems has never been done before. This thesis marks the achievement of two major goals: first, the application of software model checking to verify formally the design of a stand-alone solar photovoltaic system, including solar panel, charge controller, battery, inverter, and electric load; second, a sound, automated approach to obtaining optimal sizing of stand-alone photovoltaic systems using program synthesis. For the formal verification, we used case studies from real photovoltaic systems deployed in five different sites, ranging from $975$ W to $1,300$ W, in order to evaluate the proposed approach and to compare it with a specialized simulation tool. Different verification tools are evaluated also, in order to compare performance and soundness. Data from practical applications show the effectiveness of our proposed approach, where specific conditions that lead to failures in a photovoltaic solar system are detailed only by the automated verification method. In addition, for the use of program synthesis, we propose a variant of the counterexample guided inductive synthesis (CEGIS) approach. This variant has two phases linking the technical and the cost analysis. First, we synthesize a feasible candidate based on power reliability, but which may not attain the lowest cost. Second, the candidate is then verified iteratively with a lower bound cost via symbolic model checking. If the verification step succeeds, the lower bound is adjusted; if it fails, a counterexample provides the optimal solution. The proposed synthesis method is novel and unprecedented as it streamlines the design of photovoltaic systems. Experimental results using seven case studies demonstrate that our synthesis method can produce optimal system sizing within an acceptable run-time. We also present a comparison with a specialized simulation tool over real photovoltaic systems in order to show the effectiveness of our approach, which can provide a more detailed and accurate solution than the simulation tool. Com custos decrescentes e com melhoria de desempenho, a implantação de sistemas de energia renovável está crescendo cada vez mais rapidamente no mundo. Em 2017, pela primeira vez, o número de pessoas sem acesso a eletricidade ficou abaixo de 1 bilhão, mas os dados quanto à universalização do acesso a energia ficaram aquém das metas globais. Particular atenção é dada aos sistemas isolados solares fotovoltaicos em áreas rurais ou onde as elevadas extensões tornam a rede inviável. Ferramentas para avaliar ou dimensionar projetos de eletrificação estão disponíveis, mas elas são baseadas em simulações que não cobrem todos os aspectos do espaço de projeto. Por outro lado, o uso de métodos formais para modelar e validar qualquer tipo de sistema está crescendo com o tempo, principalmente para encontrar "bugs" em sistemas complexos de \textit{hardware} e \textit{software}: seu objetivo é estabelecer a corretude do sistema com rigor matemático. O uso de métodos formais em sistemas elétricos é um assunto recente, com pesquisas sendo publicadas apenas nos últimos quatro anos. Além disso, a síntese automatizada nunca foi usada antes para se obter um ótimo dimensionamento de sistemas solares fotovoltaicos. Esta tese marca duas conquistas principais: (1) a primeira aplicação de verificação de modelos de \textit{software} para verificar o projeto de um sistema isolado solar fotovoltaico, incluindo painel solar, controlador de carga, bateria, inversor e carga elétrica; e (2) uma abordagem confiável e automatizada para obter o dimensionamento ótimo de sistemas fotovoltaicos usando a síntese de programas onde cada componente e função de um sistema solar fotovoltaico é descrito, incluindo suas propriedades, e o modelo comportamental que representa o dimensionamento ótimo é sintetizado automaticamente. Relacionado à verificação formal, estudos de caso de sistemas fotovoltaicos reais instalados em cinco localidades diferentes são usados para avaliar a abordagem proposta e para compará-la com ferramenta de simulação especializada. Diferentes ferramentas de verificação são avaliadas também, a fim de comparar o desempenho e a confiabilidade dos resultados. Dados de aplicações práticas mostram a eficácia da abordagem proposta, onde condições específicas que levam a falhas em um sistema solar fotovoltaico são detalhadas apenas pelo método de verificação automatizado. Além disso, em relação ao uso da síntese de programas, propõe-se uma variante do método de síntese indutiva guiada por contraexemplos (CEGIS), com duas fases bem definidas: primeiro, ele sintetiza o dimensionamento de sistemas fotovoltaicos baseados em confiabilidade de energia, mas que pode não alcançar o menor custo; segundo, a solução proposta é então verificada iterativamente com um limite inferior via verificação de modelo simbólico. Se a etapa de verificação não falhar, o limite inferior será ajustado; e se falhar, o contraexemplo é fornecido com o dimensionamento ótimo, vinculando assim a resposta técnica da primeira fase à análise de custo da segunda fase. Os dados de equipamentos comerciais de diferentes fabricantes são fornecidos ao mecanismo de síntese e as soluções candidatas são derivadas da análise financeira do dimensionamento obtido. O método de síntese proposto é novo e sem precedentes para simplificar o projeto de sistemas fotovoltaicos. Resultados experimentais usando sete estudos de caso mostram que o nosso método de síntese é capaz de produzir em um tempo de execução aceitável o dimensionamento ótimo do sistema fotovoltaico, e um comparativo com uma ferramenta de simulação especializada e sistemas fotovoltaicos reais mostra a eficácia da abordagem adotada. FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas Newton Fund FAS - Fundação Amazonas Sustentável 2020-02-17T19:03:16Z 2020-01-31 Tese TRINDADE, Alessandro Bezerra. Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation. 2020. 130 f. Tese (Doutorado em Informática) - Universidade Federal do Amazonas, Manaus, 2020. https://tede.ufam.edu.br/handle/tede/7671 eng Acesso Aberto http://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Universidade Federal do Amazonas Instituto de Computação Brasil UFAM Programa de Pós-graduação em Informática |
| institution |
TEDE - Universidade Federal do Amazonas |
| collection |
TEDE-UFAM |
| language |
eng |
| topic |
Sistema solar fotovoltaico Energia renovável Verificação formal Verificação automatizada Sistemas de energia elétrica CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO Formal verification Automated verification Model checking Program synthesis Electrical systems Solar photovoltaic systems |
| spellingShingle |
Sistema solar fotovoltaico Energia renovável Verificação formal Verificação automatizada Sistemas de energia elétrica CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO Formal verification Automated verification Model checking Program synthesis Electrical systems Solar photovoltaic systems Trindade, Alessandro Bezerra Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation |
| topic_facet |
Sistema solar fotovoltaico Energia renovável Verificação formal Verificação automatizada Sistemas de energia elétrica CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO Formal verification Automated verification Model checking Program synthesis Electrical systems Solar photovoltaic systems |
| description |
With decreasing costs and increasing performance, the deployment of renewable energy systems is now growing faster than in the past decade. In 2017, for the first time, the number of people without access to electricity dipped below 1 billion, but trends in energy access still 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 or to size electrification projects are available, but they are based on simulations that do not cover all aspects of the design space. However, the use of formal methods to model and validate any system has grown with time, mainly to find bugs in sophisticated hardware and software systems: they aim to establish system correctness with mathematical rigor. The use of formal methods in electrical systems is a new subject, with published research spanning only the last four years. Moreover, the use of automated synthesis in order to obtain optimal sizing of solar photovoltaic systems has never been done before. This thesis marks the achievement of two major goals: first, the application of software model checking to verify formally the design of a stand-alone solar photovoltaic system, including solar panel, charge controller, battery, inverter, and electric load; second, a sound, automated approach to obtaining optimal sizing of stand-alone photovoltaic systems using program synthesis. For the formal verification, we used case studies from real photovoltaic systems deployed in five different sites, ranging from $975$ W to $1,300$ W, in order to evaluate the proposed approach and to compare it with a specialized simulation tool. Different verification tools are evaluated also, in order to compare performance and soundness. Data from practical applications show the effectiveness of our proposed approach, where specific conditions that lead to failures in a photovoltaic solar system are detailed only by the automated verification method. In addition, for the use of program synthesis, we propose a variant of the counterexample guided inductive synthesis (CEGIS) approach. This variant has two phases linking the technical and the cost analysis. First, we synthesize a feasible candidate based on power reliability, but which may not attain the lowest cost. Second, the candidate is then verified iteratively with a lower bound cost via symbolic model checking. If the verification step succeeds, the lower bound is adjusted; if it fails, a counterexample provides the optimal solution. The proposed synthesis method is novel and unprecedented as it streamlines the design of photovoltaic systems. Experimental results using seven case studies demonstrate that our synthesis method can produce optimal system sizing within an acceptable run-time. We also present a comparison with a specialized simulation tool over real photovoltaic systems in order to show the effectiveness of our approach, which can provide a more detailed and accurate solution than the simulation tool. |
| author_additional |
Cordeiro, Lucas Carvalho |
| author_additionalStr |
Cordeiro, Lucas Carvalho |
| format |
Tese |
| author |
Trindade, Alessandro Bezerra |
| author2 |
http://lattes.cnpq.br/4511445991061477 https://orcid.org/0000-0001-8262-2919 |
| author2Str |
http://lattes.cnpq.br/4511445991061477 https://orcid.org/0000-0001-8262-2919 |
| title |
Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation |
| title_short |
Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation |
| title_full |
Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation |
| title_fullStr |
Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation |
| title_full_unstemmed |
Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation |
| title_sort |
automated verification of stand-alone solar photovoltaic systems: optimal sizing and project validation |
| publisher |
Universidade Federal do Amazonas |
| publishDate |
2020 |
| url |
https://tede.ufam.edu.br/handle/tede/7671 |
| _version_ |
1831969850434519040 |
| score |
11.753735 |