Automated Verification of Stand-alone Solar Photovoltaic Systems: Optimal Sizing and Project Validation

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.