O objeto de estudo deste trabalho é a construção de modelos que permitam a estruturação do projeto do controle de sistemas flexíveis de manufatura que considerem não somente estados de operação normal, mas também estados anormais, isto é, em situações de falhas. Entende-se como falha o desvio de pelo menos uma propriedade do sistema que leva o mesmo a um estado de defeito, que por sua vez se define como um comportamento incomum, não projetado, do sistema sob estudo, que finalmente é manifestado como um defeito. Sistemas flexíveis de manufatura são sistemas que executam múltiplos processos visando à produção de diversos bens. O processo é um conjunto de ações de transformação que por sua parte requerem um conjunto de recursos que são compartilhados por outros processos simultaneamente. Sistemas flexíveis de manufatura envolvem um número relativamente grande de componentes, máquinas, equipamentos e operadores humanos, que interagem de maneira diversificada manipulando um grande conjunto de informação e diferentes materiais em ambientes que podem até ser agressivos. Independentemente de qualquer programa de manutenção, falhas são eventos que são possíveis de acontecer em qualquer sistema de tal natureza. Num ambiente ideal, o funcionamento de todos os componentes poderia ser monitorado com o objetivo de detectar as falhas prematuras, mas devido ao custo envolvido, isso se torna inviável. Neste sentido surge o desafio de detectar as falhas a partir da observação do contexto do funcionamento do processo, mediante a monitoração de alguns parâmetros, em geral de fácil acesso, e tomando em consideração manifestações (sintomas) das falhas de um ponto de vista qualitativo. O presente trabalho propõe a utilização de redes Bayesianas para o diagnóstico de falhas em sistemas flexíveis de manufatura. As redes Bayesianas constituem uma ferramenta útil para a representação das relações que existem entre as causas (componentes em estado de falha) e os sintomas (observações anormais do processo). A partir deste modelo, inferências podem ser feitas para o diagnóstico do sistema.Por outro lado, nos últimos anos a rede de Petri tem sido utilizada exitosamente na representação dos aspectos de controle de sistemas produtivos e particularmente de sistemas de manufatura e, desta forma, considera-se aqui tal ferramenta para a modelagem do sistema não só em condições normais de funcionamento como também para a representação do tratamento de falhas, no contexto de um sistema tolerante a anomalias do processo. Especial ênfase é dada à estruturação de uma metodologia que permita a concepção de um procedimento eficaz para a construção de modelos de controle. / The objective of the present work is the construction of models proper for the easy implementation of flexible manufacturing control systems able to handle not only with normal behavioral conditions, but with abnormal (or faulty) behavior as well. A fault is defined as a deviation of at least one system property that drives the system into an error state. An error is defined as an uncommon behavior, not expected from the system functionalities. Flexible manufacturing systems are systems that execute multiple processes for the production of several items in several ways. A process is a sequence of certain transformation tasks that require a set of resources shared simultaneously by multiple processes. In this sense, flexible manufacturing systems are constituted of a relatively great number of devices, machines, equipments and human operators that work together manipulating great quantities of information and materials. This work is usually performed in aggressive environments. So, independent of any maintenance program, faults are events that cannot be totally avoided. In an ideal environment, the monitoring of all components is the way to avoid faults. Nevertheless, due to the cost involved, this is an impossible task. In this context, there is a challenge to properly detect faults from the observation of the systems context, through the monitoring and observation of some parameters in general easy to access, including also qualitative information from operators. In the present work, it is proposed the use of Bayesian networks for the fault diagnosis in flexible manufacturing systems. Bayesian networks constitute a useful tool for the modeling of the causal relation between the causes (faulty components) and the symptoms (manifestations). Based on this model, inference can be done for the system diagnosis task. Additionally, in the last years Petri net has been successfully used for the modeling of control systems of productive systems and particularly, manufacturing control systems. In this work, beyond the use of Petri net for the modeling of normal situations of the system, Petri net is used for the modeling of the fault treatment techniques. This drives the system tolerance to faults. Especial emphasis is laid into methodological issues that allows for the structuration of a systematic procedure proper for the modeling and construction of control systems.

Dentre as tendências de uso racional de recursos, principalmente energia, e da necessidade de assegurar a produtividade e qualidade na execução de atividades produtivas, destaca-se o conceito de edifício inteligente. Este ambiente materializa o conceito de integração dos sistemas prediais potencializando a otimização dos recursos e a eficiência do trabalho humano. Neste contexto, abordagens conceituais baseadas em sistemas a eventos discretos e técnicas derivadas de rede de Petri têm sido introduzidas como uma alternativa eficaz de modelagem e análise das soluções de integração dos sistemas prediais. Um resultado expressivo destas iniciativas são os métodos propostos para a modelagem e análise de estratégias de gerenciamento de sistemas de ar condicionado, utilizando uma abordagem híbrida, onde são considerados os aspectos de sistemas a eventos discretos e as variáveis de dinâmica contínua. Contudo, as abordagens e métodos existentes são limitados a soluções específicas de implementação, como os sistemas de ar condicionado com volume de ar contínuo. Assim, o presente trabalho introduz uma extensão destas abordagens para modelar e analisar soluções de automação predial que incluem sistemas de ar condicionado com volume de ar variável. A eficiência deste método na concepção e validação destas soluções é ilustrada através de um estudo de caso. / Among the trends of rational use of resources, especially energy, and the need to ensure productivity and quality in the implementation of productive activities, there is the concept of intelligent building. This environment materializes the concept of integrating building systems, powering the optimization of resources and the efficiency of human labor. In this context, conceptual approaches that are based on systems of discreet events and techniques, which are derived from the Petri nets, have been introduced as an effective alternative to modeling and analysis of solutions of building systems integration. A significant result of these initiatives are the proposed methods for modeling and the analysis of strategies for air conditioning systems management using a hybrid approach where the aspects of systems of discreet events and the variables of continuing dynamic are considered. However, the existing methods and approaches are limited to their specific implementation solutions, such as air conditioning systems with continuous volume of air. Thus, this work introduces an extension of these approaches to model and analyze the building automation solutions that include air conditioning systems with variable volume of air. The efficiency of this method in the design and validation of these solutions is illustrated through a case study.

Submitted by Haroudo Xavier Filho (haroudo.xavierfo@ufpe.br) on 2016-03-11T15:42:40Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) jrmn_dissertacao_v.final_biblioteca.pdf: 4430943 bytes, checksum: 6417f221e28ed4c7dfe23d929b24fe60 (MD5) / Made available in DSpace on 2016-03-11T15:42:40Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) jrmn_dissertacao_v.final_biblioteca.pdf: 4430943 bytes, checksum: 6417f221e28ed4c7dfe23d929b24fe60 (MD5) Previous issue date: 2015-08-03 / FACEPE / É notável a propagação de dispositivos móveis inteligentes em todo o mundo. Em 2016, espera-se que o número de smartphones supere os 2 bilhões. A entrada desses aparelhos no mercado têm mudado o estilo de vida das pessoas, oferecendo soluções com mais facilidade e praticidade, como por exemplo, a realização de transações bancárias. A variedade e facilidade de acesso aos serviços oferecidos pelos mesmos têm ajudado nesta mudança. Além disso, o número de aplicativos nos marketplaces para satisfazer as mais diferentes necessidades dos usuários tem aumentado bastante. Por estes motivos, as aplicações móveis têm ganhado cada vez mais destaque na indústria de Tecnologia da Informação e Comunicação (TIC). Contudo, apesar da evolução da computação móvel na última década, a tecnologia das baterias desses dispositivos não evoluíram na mesma velocidade. Sendo, portanto, o curto tempo de vida das baterias uma das maiores preocupações entre fabricantes de hardware e software para dispositivos móveis. É comum o uso de modelos analíticos para analisar o comportamento dos sistemas. Modelos formais como cadeias de Markov e redes de Petri são bastante utilizadas com esse propósito. Estes tipos de modelos tem fundamentação matemática sólida, e portanto, são eficientes para realização de análises quantitativas e verificação de propriedades dos sistemas representados. Entretanto, sua construção requer conhecimento especializado por parte dos projetistas de sistemas. Por outro lado, modelos semiformais, como System Modelling Language (SysML) e Unified Model Language (UML), possuem uma notação mais flexível e são bastante difundidos no mercado. Contudo, esses modelos semiformais, por não possuírem uma fundamentação formal rígida, não oferecem suporte para o desenvolvimento de técnicas para análises numéricas e verificações de propriedades. Dessa forma, torna-se interessante a combinação do uso de modelos formais e modelos semiformais. Nesse contexto, este trabalho propõe uma abordagem para avaliação de métricas de desempenho, consumo de energia e disponibilidade de aplicações móveis utilizando modelos estocásticos. Para facilitar a construção destes modelos, a abordagem proposta adota a criação de regras de mapeamento, para obtenção de Redes de Petri stocásticas e Determinísticas (DSPNs) a partir de diagramas da SysML. Desta forma, projetistas que possuem pouco conhecimento em modelagem estocástica podem realizar análises relacionadas ao desempenho e consumo de energia de aplicações móveis de forma rápida e menos custosa que o desenvolvimento de protótipos, ainda na fase de planejamento do projeto. Por fim, são apresentados estudos de casos que demonstram a aplicabilidade da abordagem. / It is remarkable smart mobile devices spread around the world. In 2016, it is expected that the number of smartphones exceeds 2 billion. These devices entrace on the market have changed the people lifestyle, offering solutions with more ease and practicality, for example, conducting banking transactions. The variety and easy access to services offered by them have helped this change. Also, the number of applications in the marketplaces to meet the many different users needs has greatly increased. For these reasons, mobile applications have gained more prominence in the Information and Communication Technology (ICT) industry. However, despite the mobile computing progress in the last decade, the battery technology of these devices have not evolved at the same speed. It is, therefore, the short lifetime of batteries a major concern between hardware and software manufacturers to mobile devices. Analytical models are usually used to analyze the systems behavior. Formal models as Markov chains and Petri nets are widely used for this purpose. These types of models have a solid mathematical basis, and therefore, are effective in carrying out quantitative analyzes and verification systems properties. Nevertheless, their construction requires specialized knowledge by the system designers. Moreover, semiformal models, such as System Modelling Language (SysML) and Unified Model Language (UML) have a more flexible notation and are fairly widespread in the market. Meanwhile, these semi-formal models, for not having a rigid formal basis, do not support techniques for numerical analysis and property checks. Therefore, it becomes interesting to use the combination of formal and semi-formal models. In this context, this work proposes an approach to evaluation performance, power consumption and availability metrics of mobile applications using stochastic models. In order to facilitate construction of such models, the proposed approach adopts the creation of mapping rules for obtaining Stochastic Petri Nets and deterministic (DSPNs) from SysML diagrams. In this way, designers who have little knowledge in stochastic modeling can perform analyzes related to the performance and power consumption in mobile applications quickly and less costly to develop prototypes, still in the project planning phase. Finally, case studies are presented to demonstrate the approach applicability.

Made available in DSpace on 2014-06-12T15:52:45Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Os sistemas de transferência eletrônica de fundos (TEF) promovem benefícios financeiros para as instituições que utilizam esse serviço e conveniências para seus clientes. Os sistemas TEF realizam operações de crédito e débito em contas bancárias através de terminais de pontos de vendas (PDVs) em diferentes empresas. Assim, a avaliação de desempenho de sistemas TEF tem fundamental importância para as empresas que promovem o serviço de transferência eletrônica de fundos, uma vez que os recursos computacionais devem ser utilizados eficientemente, objetivando atingir os requisitos definidos nos acordos de nível de serviço (SLA). A ocorrência de eventos de falhas podem causar uma severa degradação no desempenho de sistemas. Assim, os resultados da modelagem de sistemas sem considerar os efeitos da dependabilidade sobre o desempenho são incompletos ou imprecisos. Este trabalho apresenta uma metodologia para avaliação da performabilidade composta de um método para avaliação de desempenho, um método para avaliação da dependabilidade e uma técnica de decomposição e composição. Este trabalho também apresenta dois modelos estocasticos expolinomiais para avaliação de performabilidade os quais são o modelo de desempenho de sistemas TEF e o modelo de dependabilidade de sistemas TEF. O modelo de desempenho de sistemas TEF proporciona a avaliação do desempenho dos recursos de processamento e armazenamento do servidor TEF, considerando variações na carga de trabalho (transações comerciais de crédito e débito). Já o modelo de dependabilidade de sistemas TEF promove a avaliação dos efeitos da ocorrência de eventos de falhas e de uma política de manutenção na disponibilidade e confiabilidade da infraestrutura de sistemas TEF. Os modelos de desempenho e de dependabilidade são combinados para a avaliação do impacto da dependabilidade no desempenho de sistemas TEF. A política de manutenção é empregada para prevenir a ocorrência de eventos de falhas no sistema TEF e permitir a recuperação de falhas para assegurar as expectativas de desempenho dos clientes através dos ajustes dos intervalos entre manutenções preventivas, dos intervalos entre substituições dos equipamentos, do número máximo de manutenções preventivas antes da substituição dos equipamentos, do tempo médio para reparo, do dimensionamento da equipe de manutenção e dos custos relacionados às manutenções. Estudos de caso são apresentados para análise do impacto das variações da carga de trabalho no desempenho de sistemas TEF, para análise do impacto de uma política de manutenção na performabilidade de sistemas TEF e para análise dos efeitos das variações de temperatura na performabilidade de sistemas TEF

Made available in DSpace on 2014-06-12T15:56:43Z (GMT). No. of bitstreams: 2 arquivo2981_1.pdf: 3215822 bytes, checksum: 207b7ae6534fc85e3430543b64c88b38 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2010 / A procura por softwares com maior qualidade tem motivado a definição de métodos e técnicas para o desenvolvimento de softwares que atinjam os padrões de qualidade impostos. Com isso, o interesse pela atividade de teste de software vem aumentando nos últimos anos. As fábricas de software enfrentam dificuldades na elaboração de processos de testes adequados ao projeto de maneira que sejam efetivos com relação à qualidade do produto e, ao mesmo tempo, tenham execução eficiente. Esses aspectos concorrentes podem afetar os níveis de qualidade almejado ou induzir o desenvolvimento de processos rebuscados e ineficientes. Parte desse problema ocorre tanto devido à dificuldade enfrentada pelas organizações na definição de processos a cada projeto particular, quanto pela ausência de mecanismos que possibilitem a provisão de meios para escolha das alternativas mais convenientes a cada projeto particular em termos de desempenho e critérios de qualidade. Dessa forma, ambientes que proporcionem a avaliação do desempenho dos processos e que possibilitem estimativa do uso de recursos são mecanismos que concorrem para melhoria dos índices de qualidade e produtividade das organizações. Modelos de execução de processo voltados para estimativa de desempenho que levem em consideração combinações de cenários diversos e ativos podem trazer ganhos substanciais de produtividade tanto na customização dos processos quanto na efetividade do processo definido para o projeto. Este trabalho propõe uma metodologia de avaliação de desempenho aplicada a Processos de Testes de Software. Com a aplicação da metodologia proposta, é possível verificar o impacto de mudanças no processo, avaliar o desempenho do processo de testes, realizar simulações com o objetivo de obter estimativas mais precisas e, principalmente, ajudar na garantia da qualidade do produto. Além disso, essa metodologia possibilitará a avaliação de diferentes alternativas de implementações, bem como a verificação de melhor composição de recursos pessoais para as atividades do processo. Isso tudo pode ser realizado sem a necessidade da real implementação do processo, tornando mais ágil e barato todo o processo

Made available in DSpace on 2014-06-12T15:59:31Z (GMT). No. of bitstreams: 2 arquivo5135_1.pdf: 1049051 bytes, checksum: e5be25e2aa87cb17b0788411f129a4a8 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / Atualmente, sistemas embarcados são ubíquos. Em outras palavras, eles estão em todos os lugares. Desde utilitários domésticos (ex: fornos microondas, refrigeradores, videocassetes, máquinas de fax, máquinas de lavar roupa, alarmes) até equipamentos militares (ex: mísseis guiados, satélites espiões, sondas espaciais, aeronaves), nós podemos encontrar um sistema embarcado. Desnecessário afirmar que a vida humana tem se tornado mais e mais dependente desses sistemas. Alguns sistemas embarcados são classificados como sistemas de tempo real, onde o comportamento correto depende não somente da integridade dos resultados, mas também nos tempos em que tais resultados são produzidos. Em sistemas embarcados de tempo real críticos, se as restrições temporais não forem satisfeitas, as conseqüências podem ser desastrosas, incluindo grandes danos aos equipamentos ou mesmo perdas de vidas humanas. Devido a tarefas que possuem alta taxa de utilização de processador, alguns sistemas embarcados (ex: dispositivos médicos) precisam ser compostos de mais de um processador para obter performance aceitável e, no caso de sistemas embarcados de tempo real críticos, para satisfazer as restrições temporais críticas. Entretanto, questões adicionais precisam ser consideradas para lidar com um ambiente multiprocessado, tal como comunicação entre processadores e sincronização. Nessa dissertação, um método de síntese de software baseado no formalismo matemático redes de Petri com tempo é apresentado para lidar com sistemas embarcardos de tempo real críticos com múltiplos processadores. A abordagem inicia a partir de uma especificação (usualmente composta de tarefas concorrentes e comunicantes) e automaticamente gera o código fonte de um programa considerando: (i) as funcionalidades e restrições; e (ii) o suporte operacional para execução das tarefas em um ambiente multiprocessado. Síntese de software é uma alternativa para sistemas operacionais especializados para dar suporte a execução de um programa. Sistemas operacionais são usualmente genéricos e podem introduzir atrasos no tempo de execução, e ao mesmo tempo produzir alto consumo de memória. Por outro lado, a síntese de software é uma alternativa de projeto, dado que este método automaticamente gera o código fonte do programa, satisfazendo a funcionalidade, as restrições especificadas, o suporte para execução, e a minimização dos atrasos e uso de memória

O gerenciamento de projetos assume um papel cada vez mais importante nas atividades empresariais. Os projetos têm papel importante na sobrevivência da empresa. Assim, uma sistemática eficiente para o gerenciamento de seus projetos atenderá aos padrões do mercado na questão de custos e prazo. A eficiência dos sistemas produtivos também tem grande importância. Neste cenário as empresas devem possuir uma sistemática eficiente para a otimização do sistema produtivo a fim de obter-se um sistema eficaz. O presente trabalho traz duas propostas para melhoria destes problemas, o primeiro é o desenvolvimento de uma metodologia para gerenciamento de projetos e o segundo uma metodologia de otimização do sistema produtivo utilizando Redes de Petri auxiliado por simulação discreta. Para comprovar a eficácia destas propostas, um estudo de caso foi realizado em uma empresa. / The management of projects assumes a role nowadays each more important time in the enterprise activities. In manufacture companies who work in an environment under order, the projects have important paper in the survival of the company. Thus, these companies must possess an efficient systematics for the management of its projects, in order to take care of to the standards, each limited time more, of cost, stated period and quality of its customers. The efficiency of the productive systems also has great importance in the activities entrepreneurs now a day. The companies who do not present efficient a productive system do not obtain to compete in equality in this globalizado world, in this scene the companies must possess an efficient systematics for the optimization and the simulation of the productive system in order to arrive at an efficient system. The present work brings two proposals for improvement of these problems, the first one is developing of a methodology for management of projects and as a methodology of optimization of the productive system using nets of Petri assisted for discrete simulation, and to prove the effectiveness of these proposals a case study it was elaborated in a company in order to get itself resulted for the evidence of the elaborated proposals.

CoordenaÃÃo de AperfeiÃoamento de NÃvel Superior / Na conjuntura atual à possÃvel observar o grave problema de escassez energÃtica com o qual a humanidade se depara. Os derivados de petrÃleo estarÃo se exaurindo nas prÃximas dÃcadas e o tempo geolÃgico necessÃrio para a revitalizaÃÃo do estoque desta energia fÃssil a inviabiliza no longo prazo. Neste contexto, a busca por fontes renovÃveis de energia, como, por exemplo, o biodiesel, torna-se de suma importÃncia. Diversas oleaginosas podem ser empregadas para a produÃÃo de biodiesel, dentre as quais pode ser destacada a mamona. O agronegÃcio da mamona constitui-se numa cadeia produtiva complexa, tornando necessÃrios esforÃos dirigidos para a estruturaÃÃo desta cadeia ainda incipiente. Sistemas a Eventos Discretos (SED) vÃm sendo amplamente utilizados na modelagem de cadeias produtivas, apoiando o processo de planejamento e de gerenciamento de tais sistemas. Dentre as tÃcnicas de modelagem de SED, as redes de Petri destacam-se por propiciarem uma representaÃÃo compacta de um sistema e por permitirem a sua simulaÃÃo e anÃlise. O controle supervisÃrio de SED consiste em sintetizar um supervisor que coordene as atividades de subsistemas de modo que o sistema geral satisfaÃa um conjunto de especificaÃÃes. O objetivo geral deste trabalho foi elaborar um modelo, baseado em redes de Petri, que permitisse o controle supervisÃrio da Cadeia Produtiva do Biodiesel da Mamona (CP/BDMA), com vistas a garantir sua efetividade. Foi desenvolvido um novo mÃtodo de controle supervisÃrio baseado em redes de Petri coloridas, denominado RestriÃÃes de Controle sobre Cores Decompostas (RCCD), sendo tambÃm proposta uma arquitetura para o controle supervisÃrio em sistemas logÃsticos. Idealizou-se um modelo teÃrico da CP/BDMA no qual foi possÃvel ressaltar a importÃncia da coordenaÃÃo de atividades logÃsticas no Ãmbito da cadeia. Foram estabelecidas especificaÃÃes funcionais para o sistema e, em seguida, efetuou-se a avaliaÃÃo do seu desempenho, com base no tempo de ciclo, atravÃs da simulaÃÃo de diversos cenÃrios operacionais. Como conclusÃes, pode-se ressaltar que o mÃtodo RCCD constitui-se em uma eficiente abordagem para o controle de SED, que a modelagem proposta permitiu uma maior compreensÃo acerca do sistema em estudo e que o controle supervisÃrio à uma tÃcnica que pode subsidiar o processo de tomada de decisÃo no Ãmbito CP/BDMA, sendo tambÃm aplicÃvel a outras cadeias produtivas agroindustriais / Nowadays many countries present critical problems related to energy demand-supply equilibrium. The reserves of petroleum-based products are unable to face future demand for the next decades. So, the search for alternative sources of energy has been strongly directed to biodiesel. Several fruit oils can be used as a source for biodiesel production and the castor bean is an example. The castor bean agribusiness is a complex commodity chain, making necessary researches for the conception of this incipient chain. Discrete Event Systems (DES) are largely used in the modeling of commodity chains, aiding the planning and the manage of these systems. Among the DES modeling techniques, the Petri nets stands out for as making a easier a compact representation of a system and for permitting its simulation and analysis. The supervisory control aims for synthesize a supervisor that coordinate the activities of the subsystems in order to satisfy a set of specifications in a general system. The general purpose of this work was create a model, based on Petri nets, that permit the supervisory control of Castor Bean Biodiesel Supply Chain (CBB/SC) in order to guarantee its efficiency and efficacy. It was developed a new method for the supervisory control based on colored Petri nets, called Constraints of Control on Decomposed Colors (CCDC). Also, it was proposed a new framework for the supervisory control in logistics systems. Functional specifications were established for found the system which had its performance evaluated, based on the lead time, through simulation of several operational scenarios. As conclusion, it seems clear that the CCDC method is a consistent approach for DES control, the proposed model helps in a better comprehension about the system in analysis and the supervisory control is a theory that can aid the decision making process in similar chains as CBB/SC

Made available in DSpace on 2015-04-11T14:03:15Z (GMT). No. of bitstreams: 1 DISSERTACAO MARCELO.pdf: 1313111 bytes, checksum: ddf9a22433355413e807d3bd27951a01 (MD5) Previous issue date: 2008-12-15 / Fundação de Amparo à Pesquisa do Estado do Amazonas / Embedded systems have undeniable relevance in modern society. They have temporal constraints (as long as they are real time ones), power consumption management, size, weight, etc which make their design more complex than the design of their desktop peers. Given the huge number of requirements of all kinds, the high complexity of embedded software as well as the big possibilities of critical damages in case of flaws and, at last, the even bigger pressure of market for new products faster, it make necessary methods which can assure correct, fast but intuitive specification and conception of designs. Considering this, this work aims to provide a method which contribute to the state of art. The goal of the proposed method is to provide an approach which gather an specification of an embedded software in a semi-formal, object-oriented and Industry-accepted notation, which is Unified Modeling (UML), specifically their Sequence Diagram notation which is able to capture dynamic aspects of a system and a mecanism of translation of this notation into a formal one, called SMV, apropriate for being used by the SMV model checker. The goal of the method is also provide an translation scheme of the sequence diagrams into another formal notation, the so called Petri Nets notations. Petri Net notation is well suited to formal verification. Finally, the goal of the method is to provide a mechanism of translation of high level properties queries into formal notation CTL. Property queries are only qualitative. All these functionalities are implemented in a tool called Ambiente de Verificação Formal de Software Embarcado. / Os sistemas embarcados possuem inegável importância na sociedade atual. Eles possuem restrições temporais (quando são de tempo real), de gerência de consumo de energia, tamanho, peso etc que tornam o seu projeto e concepção mais complexos do que os sistemas convencionais. Dado o grande número de requisitos de todos os tipos, a alta complexidade dos softwares embarcados desenvolvidos bem como a grande possibilidade de catástrofes significativas em caso de falha e por fim a grande pressão de mercado por produtos cada vez mais rápido, fazem-se necessários métodos que possam assegurar uma correta, rápida porém intuitiva especificação e concepção dos projetos. Diante disso, o presente trabalho visa prover um método que acrescente ao atual estado da arte. O objetivo do método então é prover uma abordagem que colete uma especificação de software embarcado em uma notação semi-formal, orientada a objetos e amplamente aceita pela Indústria, que é a Unified Modeling Language (UML), especificamente com seu Diagrama de Sequência, o qual é apto para capturar os aspectos dinâmicos de um sistema e um mecanismo de tradução dessa notação para a notação formal SMV, apta a ser utilizada pelo model checker de mesmo nome. O objetivo do método é prover também um esquema de tradução dos diagramas de sequência em UML para uma notação formal, no caso a notação de Redes de Petri, o qual é adequada para verificação formal, gerando saídas de arquivos nos formatos APNN e PNML. O formato APNN é adequado para ser usado no Model Checking Kit (MCK). Por fim, prover um esquema de tradução consultas de propriedade em alto nível para o formato de CTL puro adequado para ser usado no MCK e um programa em SMV e sua especificação 7 em CTL, formatos aptos a serem usados no model checker SMV. A verificação de propriedades é apenas qualitativa, isto é, que verificará apenas propriedades de execução do software embarcado, em oposição às propriedades quantitativas de tempo por exemplo, comuns em softwares de tempo-real. Todas essas funcionalidades são realizadas por uma ferramenta, chamada Ambiente de Verificação Formal de Software Embarcado.

Os modernos sistemas de mediÃÃo, proteÃÃo, comando, controle e supervisÃo (MPCCS) tÃm contribuÃdo de forma significativa para o aumento da seguranÃa, confiabilidade e continuidade de serviÃo dos sistemas elÃtricos de potÃncia. O sistema de proteÃÃo à parte relevante desse sistema multifuncional, o qual tem como objetivo principal manter a integridade do sistema elÃtrico quando submetido a um distÃrbio, garantindo a seguranÃa de pessoas e assegurando a continuidade de serviÃo da porÃÃo nÃo envolvida no problema. Para tanto, o sistema de proteÃÃo deve atender a alguns requisitos bÃsicos tais como: boa seletividade e coordenaÃÃo, rapidez na atuaÃÃo, sensibilidade para proteger a maior zona de proteÃÃo possÃvel e confiabilidade. No sistema de proteÃÃo, um componente assume uma posiÃÃo de destaque: o relà de proteÃÃo digital. à neste componente que sÃo configurados os ajustes necessÃrios para o correto funcionamento do esquema de proteÃÃo de um dado sistema elÃtrico. Os relÃs de proteÃÃo digitais sÃo equipamentos multifuncionais, que possuem diversas funÃÃes de proteÃÃo, mediÃÃo de grandezas elÃtricas, registros oscilogrÃficos, supervisÃo, controle e comunicaÃÃo. AlÃm de todos estes recursos, os relÃs digitais dispÃem de mÃltiplos grupos de ajustes que podem ser previamente configurados conforme necessidade operacional. A mudanÃa de grupo de ajuste de um relà à um recurso amplamente utilizado pelas Ãreas de proteÃÃo das empresas do setor elÃtrico, possibilitando uma otimizaÃÃo do ajuste do sistema de proteÃÃo, compatibilizando-o Ãs diversas topologias assumidas pelo sistema elÃtrico apÃs uma falta ou retirada intencional de algum componente da rede. Atualmente este procedimento à realizado de forma manual, tornando-o vulnerÃvel à falha humana, podendo ter como consequÃncia desligamentos de grandes blocos de carga por falha de coordenaÃÃo, com graves prejuÃzos para os indicadores da qualidade de serviÃo de duraÃÃo e frequÃncia de interrupÃÃo, DEC e FEC, e para a imagem da empresa. Neste trabalho à apresentado um sistema, baseado em Redes de Petri Coloridas, capaz de realizar a mudanÃa automÃtica entre grupos de ajustes de um sistema de proteÃÃo a partir da mudanÃa de topologia do sistema elÃtrico. O sistema desenvolvido monitora a topologia da rede elÃtrica, em tempo real, a partir das informaÃÃes de estado dos disjuntores. Para qualquer alteraÃÃo na configuraÃÃo da rede elÃtrica, que caracterize necessidade de alteraÃÃo no sistema de proteÃÃo, automaticamente sÃo enviados sinais de comando para os relÃs, alterando os grupos de ajustes ativos de um conjunto predefinido, de modo a se obter a melhor graduaÃÃo de proteÃÃo possÃvel para a porÃÃo correspondente do sistema elÃtrico afetado pela alteraÃÃo de topologia. / The modern systems of measurement, protection, command, control and supervision (MPCCS) have contributed in a meaningful way to increase the security and reliability of the power systems. The most important part of this multifunctional system is the protection system, which has as the main goal to maintain the power system integrity when it is under a disturbance, assuring the peopleâs safety as well as the continuation of the services to the part of the system not involved in the disturbance. For this, the protection system must fulfill some basic requirements such as: proper selectivity and coordination, prompt response, sensitivity to protect the largest zone as possible and reliability. In a system protection, one component takes on a prominent position, given its functional importance: the digital protection relay. It is in this device where the necessary adjustments are configured for proper operation of the protection scheme of a given electrical power system. The digital relays are devices that have several protection functions, with multiple levels of settings, measurements, oscillography, supervision, control and communication. Besides all these features, the digital relays have multiple groups of settings that can be previously configured and switched among them, according to operational needs. The changing of setting group in a relay is a very important resource at a protection system, extensively used by protection sectors of companies in the power sector, allowing the optimization of the protection system setting, making it compatible to a new topology taken on by the system after a fault or an intentional removal of some system component. Nowadays this procedure is performed manually, making it vulnerable to human errors that might occur as a consequence of an outage, with serious effect in the system performance indices. In this sense this work presents a system, based on Colored Petri Nets, able to automatically change the setting groups of a protection system when the power network topology changes. This system monitors in real time the status of the circuit breakers in order to take the decision whether a meaningful change in the network topology has taken place. If so, a command is automatically sent to the relays to change the active group setting so as to maintain a suitable coordination of the protection system.