???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/7671
Tipo do documento: Tese
Título: Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation
Título(s) alternativo(s): Verificação Automática de Sistemas Solares Fotovoltaicos Off-grid: Dimensionamento Ótimo e Validação de Projeto
Autor: Trindade, Alessandro Bezerra 
Primeiro orientador: Cordeiro, Lucas Carvalho
Primeiro membro da banca: Mota, Edjard de Souza
Segundo membro da banca: Barreto, Raimundo da Silva
Terceiro membro da banca: Silva, Sidelmo Magalhães
Quarto membro da banca: Macêdo, Wilson Negrão
Resumo: 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.
Abstract: 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.
Palavras-chave: Sistema solar fotovoltaico
Energia renovável
Verificação formal
Verificação automatizada
Sistemas de energia elétrica
Área(s) do CNPq: CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
???metadata.dc.subject.user???: Formal verification
Automated verification
Model checking
Program synthesis
Electrical systems
Solar photovoltaic systems
Idioma: eng
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Instituto de Computação
Programa: Programa de Pós-graduação em Informática
Citação: 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.
Tipo de acesso: Acesso Aberto
Endereço da licença: http://creativecommons.org/licenses/by-nc-nd/4.0/
URI: https://tede.ufam.edu.br/handle/tede/7671
Data de defesa: 31-Jan-2020
Appears in Collections:Doutorado em Informática

Files in This Item:
File Description SizeFormat 
Tese_AlessandroTrindade_PPGI.pdfTese_AlessandroTrindade_PPGI2,96 MBAdobe PDFThumbnail

Download/Open Preview


This item is licensed under a Creative Commons License Creative Commons