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.

Submitted by Wagner Junior (wagner.junior@unioeste.br) on 2018-11-30T17:04:04Z No. of bitstreams: 2 Claudia_Beatriz_Bozz_2018.pdf: 4791914 bytes, checksum: 0affba2e984ec7e6beefa83d0c3bdfeb (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-11-30T17:04:04Z (GMT). No. of bitstreams: 2 Claudia_Beatriz_Bozz_2018.pdf: 4791914 bytes, checksum: 0affba2e984ec7e6beefa83d0c3bdfeb (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2018-07-26 / Real time systems that have continuous behavior associated with discrete elements are called hybrid systems. Among them, in this master’s research, a hydraulic system has been chosen as an object of study in order to perform the reliability analysis of it through modeling and formal verification. Much as several models for the reliability analysis of complex systems have been proposed in the literature, most of them are not suitable to represent the system when its behavior needs to be expressed by means of continuous variables, like the case of hybrid systems. Generally, simulation and experimental testing are used to analyze systems, and they give only approximate results from a large amount of samples. To eliminate the limitations of these techniques, the formal verification is an effective alternative, since it is characterized by performing a sweep in all possible states of the system automatically, verifying the behavior as a whole. The UPPAAL STRATEGO toolkit for modelling by stochastic hybrid automata and model checking has been used in this work, both classic formal verification and statistical formal verification. A benckmark has been used as object of study. Initially, the system has been modelling and its behavior (physical and controlled) verified through simulation and formal verification (property specification and model checking). The reliability parameters obtained in the statistical analysis of the system failures have been compared with results of literature, presenting a dispersion less than 2.5%, so it can be verify that the methodology used and the models constructed were adequate to analyze the reliability of this system hybrid.In a second step of this work, the probability distribution of failure of the components have been modified, in order to become the system more reliable with real hydraulic systems, and estimate the optimum mean time between maintenance (MTBM) of this system. Thus, it’s possible to conclude that the methodology is adequate to perform the reliability analysis of the hydraulic system, being that model checking is effective to estimate the reliability parameters of the hydraulic system. / Sistemas de tempo real que possuem comportamento contínuo associado com elementos de características discretas são chamados de sistemas híbridos. Dentre estes, nesta pesquisa de mestrado, optou-se pelo emprego de um sistema hidráulico como objeto de estudo a fim de realizar a análise de confiabilidade do mesmo a partir de modelagem e verificação formal. Por mais que diversos modelos para a análise de confiabilidade de sistemas complexos tenham sido propostos na literatura, a maioria não são adequados para representar sistemas em que o comportamento é expresso em variáveis contínuas, como é o caso dos sistemas híbridos. De modo geral, para a análise de sistemas, a simulação e os testes experimentais são comumente utilizados, e geram apenas resultados aproximados a partir de uma grande quantidade de amostras. Para eliminar as limitações destas técnicas, a verificação formal é uma alternativa eficaz, visto que é caracterizada por realizar uma varredura em todos os estados possíveis do sistema de forma automática, verificando o comportamento como um todo do mesmo. Neste trabalho, foi utilizada a ferramenta computacional UPPAAL STRATEGO para a modelagem por autômatos estocásticos híbridos e verificação dos modelos, tanto verificação formal clássica como estatística. Um modelo padrão (benchmark) foi utilizado como objeto de estudo. Inicialmente o sistema foi modelado e seu comportamento (físico e controlado) verificado através da simulação e verificação formal (especificação de propriedades e verificação de modelos). Os parâmetros de confiabilidade obtidos na análise estatística de falha do sistema foram comparados com outros existentes na literatura, apresentado uma dispersão inferior a 2,5%, logo pôde se verificar que a metodologia empregada e os modelos construídos foram adequados para análise de confiabilidade deste sistema hibrido. Em uma segunda etapa do trabalho, foi modificada a distribuição de probabilidade de falha dos componentes, a fim de tornar o sistema mais fidedigno com sistemas hidráulicos reais, e estimar o tempo médio entre manutenções (MTBM – Mean Time Between Maintenance) ideal deste sistema. Portanto, conclui-se que a metodologia empregada foi adequada para realizar a análise de confiabilidade do sistema hidráulico, sendo efetivo levantar os parâmetros de confiabilidade através da verificação de modelos.