| Summary: | Submitted by Miriam Lucas (miriam.lucas@unioeste.br) on 2018-02-22T14:23:15Z
No. of bitstreams: 2
Felipe_Crestani_dos_Santos_2017.pdf: 5495370 bytes, checksum: 82f81445874bba45497cda5c8d784d2f (MD5)
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) === Made available in DSpace on 2018-02-22T14:23:15Z (GMT). No. of bitstreams: 2
Felipe_Crestani_dos_Santos_2017.pdf: 5495370 bytes, checksum: 82f81445874bba45497cda5c8d784d2f (MD5)
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Previous issue date: 2017-11-17 === The main line of research of this work is the study of approaches for supporting the development
and analysis of the Power System Protection. In general, this process is carried out
through of a large number of simulations involving various operating scenarios. The main limitation
of this technique is the impossibility of coverage of all behavior of the system under
analysis. In this context, this work proposes the use of Model Checking as a tool to support
the procedure of development of power system protection schemes, principally in the sense of
proving the security requirements and temporal deterministic expected behavior. Model Checking
is a verification technique that explores exhaustively and automatically all possible system
states, checking if this model meets a given specification. This work focuses on this two pillars
of the Model Checking: to choose an appropriate modeling formalism for representation
of the power system protection and how to describe the specification in temporal-logic for the
verification process. With regard to the modeling formalism, the power system protection will
be represented by the Hybrid Automata theory, while the verification tool adopted will be Statistical
Model Checking, by the UPPAAL STRATEGO toolkit. It is underlined that this work
is limited to the modeling of individual components of the power system protection, such that
18 models of the devices and protocols like communication bus (LAN), time synchronization
protocol (PTP) and IEC 61850 communication protocols (SV and GOOSE) and Logical Nodes
of power system protection, and 13 auxiliaries models, which emules the stochastic behavior
to subsidise the verification process. The methodology of modelling adopted guarantees the
effective representation of the components behaviour of power system protection. For this, the
results of Model Checking process were compared with behavioral requirements defined by
standards, conformance testings and paper related to the area. With regard to the contributions
of this work, were identified three researches areas that could use the models developed in this
work: i) implementation of power system protection schemes; ii) achievement of conformance
testing; and iii) indication of the parameterization error of the power protection system scheme. === A linha de pesquisa abordada neste trabalho aponta para o estudo e desenvolvimento de ferramentas
que subsidiem a proposição e validação de Sistemas de Proteção de Sistemas de Energia
Elétrica. Em geral, este processo é realizado mediante simulações computacionais envolvendo
diversos cenários de operação e distúrbios, tendo como principal limitação a impossibilidade de
representar todos os caminhos de evolução do sistema em análise. Nesse contexto, propõe-se o
emprego da técnica de Modelagem e Verificação Formal como ferramenta de suporte ao projeto,
análise e implementação de estratégias de proteção, principalmente no sentido de comprovar se
a estratégia atende os requisitos de segurança e comportamento determinístico temporal esperado.
Em síntese, o método consiste na verificação de propriedades descritas em lógicas temporais,
sob uma abstração apropriada (formalismo) do comportamento do sistema. Esta dissertação
possui enfoque nestes dois requisitos: modelagem do sistema de proteção através de um
formalismo adequado e tradução dos requisitos do comportamento desejado em propriedades
descritas em lógica temporal. Com relação ao formalismo de apoio, a modelagem do sistema
de proteção é baseada em uma abstração de Autômatos Temporizados Híbridos. Como ferramenta
de validação, adota-se a técnica de Verificação Formal Estatística, através do software
UPPAAL STRATEGO. Salienta-se que este trabalho se delimita apenas na modelagem e validação
individual dos principais equipamentos de um sistema de proteção, sendo 18 modelos de dispositivos
e protocolos como barramentos de comunicação (LAN), protocolo de sincronização
de tempo PTP, protocolos de comunicação baseados em IEC 61850 e funções de proteção, e 13
modelos auxiliares que implementam um comportamento estocástico para subsidiar o processo
de validação do sistema de proteção. O desenvolvimento dos modelos se deu através de uma
abordagem sistemática envolvendo processos de simulação e verificação das propriedades sob
o modelo em análise. Através desta metodologia, garante-se que os modelos desenvolvidos representam
o comportamento esperado de seus respectivos dispositivos. Para isso, os resultados
do processo de verificação foram comparados com requisitos comportamentais definidos por
normas, testes de conformidade em equipamentos/protocolos e trabalhos acadêmicos vinculados
à área. Com relação às contribuições do trabalho, identificou-se três linhas de pesquisa que
podem fazer o uso dos modelos desenvolvidos: i) implementação de novas estratégias de proteção;
ii) realização de testes de conformidade em equipamentos externos à rede de autômatos;
e iii) indicação de erros de parametrização do sistema de proteção.
|
|---|
