Os sistemas produtivos (SPs) podem utilizar controladores programáveis (CPs) como dispositivos de realização do controle. Neste contexto, programas de controle executados por estes CPs podem ser desenvolvidos de forma que não estejam em conformidade com as especificações de projeto, o que poderá provocar o surgimento de erros funcionais associados à execução de tais programas de controle, erros estes que podem levar os SPs sob controle a um estado que poderá implicar em acidentes envolvendo equipamentos, pessoas e o meio-ambiente. Esta questão tem motivado o surgimento de diversas abordagens para identificar a existência de erros em programas de controle de CPs, de forma a permitir a correção destes erros e garantir, conseqüentemente, maior confiabilidade operacional. O presente trabalho tem por objetivo identificar a existência de erros em programas de controle baseados em LD (Ladder Diagram). Para isto, propõe-se um procedimento de desenvolvimento de modelos baseados em máquinas de estados finitos estendidas (MEFEs), que são gerados a partir do mapeamento de cada um dos rungs contidos no programa de controle que se deseja identificar erros. Uma vez desenvolvidos os modelos em MEFEs, torna-se possível a utilização de uma ferramenta computacional de verificação, própria para estabelecer se os modelos verificados satisfazem determinadas proposições estabelecidas em lógica temporal. Uma proposição em lógica temporal está relacionada a um estado específico do programa de controle modelado, sendo que o objetivo da verificação é o de estabelecer se a proposição estipulada é atendida ou não. Se um determinado estado específico for, por exemplo, um estado indesejado do programa de controle modelado, e este estado for possível de ser alcançado como resultado do processo de verificação realizado, isto impactará na não conformidade do programa de controle com as especificações comportamentais estipuladas na forma de proposição em lógica temporal, indicando haver, portanto, um erro neste programa de controle modelado. Palavras-chave: Controladores programáveis. Linguagem de programação LD. Modelagem e verificação de máquinas de estados finitos estendidas (MEFEs). / Productive systems (PS) can use programmable logic controllers (PLCs) as the devices of accomplishment of the control. In this context, control programs executed by these PLCs can be developed in a way so that they can be in non-conformity with the project specifications, and this fact may result in functional errors related to the control programs execution. These errors can take the PS under control to a state which can lead into accidents involving equipment, people and the environment. This fact has motivated the appearance of different approaches so as to identify the existence of these errors in PLC control programs so that they can be corrected and assure a greater operational reliability. This work aims at identifying the existence of errors in control programs based on Ladder Diagram (LD). In order to accomplish that, a modeling procedure that generates extended finite state machines (EFSMs) is proposed from the mapping of each one of the rungs in the control program whose errors are to be identified. Once the models based on EFSMs are developed it becomes possible to use a computational verification tool, specifically designed to determine if the verified models fulfill determined propositions established in temporal logic. A proposition in temporal logic is related to a specific state of the modeled control program and the objective of the verification is to establish whether the proposition is fulfilled or not. If a determined specific state, for example, is an unwanted state of the modeled control program and if this state is reachable as a result of the verification process, this will impact in the non-conformity of the control program with the behavior specifications established in a temporal logic proposition, indicating an error in this modeled control program.

O objetivo deste trabalho é tornar possível a inserção de um robô humanoide para auxiliar pacientes em sessões de fisioterapia. Um sistema robótico é proposto que utiliza um robô humanoide, denominado NAO, visando analisar os movimentos feitos pelos pacientes e corrigi-los se necessário, além de motivá-los durante uma sessão de fisioterapia. O sistema desenvolvido permite que o robô, em primeiro lugar, aprenda um exercício correto de fisioterapia observando sua execução por um fisioterapeuta; em segundo lugar, que ele demonstre o exercício para que um paciente possa imitá-lo; e, finalmente, corrija erros cometidos pelo paciente durante a execução do exercício. O exercício correto é capturado por um sensor Kinect e dividido em uma sequência de estados em dimensão espaço-temporal usando k-means clustering. Estes estados então formam uma máquina de estados finitos para verificar se os movimentos do paciente estão corretos. A transição de um estado para o próximo corresponde a movimentos parciais que compõem o movimento aprendido, e acontece somente quando o robô observa o mesmo movimento parcial executado corretamente pelo paciente; caso contrário o robô sugere uma correção e pede que o paciente tente novamente. O sistema foi testado com vários pacientes em tratamento fisioterapêutico para problemas motores. Os resultados obtidos, em termos de precisão e recuperação para cada movimento, mostraram-se muito promissores. Além disso, o estado emocional dos pacientes foi também avaliado por meio de um questionário aplicado antes e depois do tratamento e durante o tratamento com um software de reconhecimento facial de emoções e os resultados indicam um impacto emocional bastante positivo e que pode vir a auxiliar pacientes durante tratamento fisioterapêuticos. / This dissertation develops a robotic system to guide patients through physiotherapy sessions. The proposed system uses the humanoid robot NAO, and it analyses patients movements to guide, correct, and motivate them during a session. Firstly, the system learns a correct physiotherapy exercise by observing a physiotherapist perform it; secondly, it demonstrates the exercise so that the patient can reproduce it; and finally, it corrects any mistakes that the patient might make during the exercise. The correct exercise is captured via Kinect sensor and divided into a sequence of states in spatial-temporal dimension using k-means clustering. Those states compose a finite state machine that is used to verify whether the patients movements are correct. The transition from one state to the next corresponds to partial movements that compose the learned exercise. If the patient executes the partial movement incorrectly, the system suggests a correction and returns to the same state, asking that the patient try again. The system was tested with multiple patients undergoing physiotherapeutic treatment for motor impairments. Based on the results obtained, the system achieved high precision and recall across all partial movements. The emotional impact of treatment on patients was also measured, via before and after questionnaires and via a software that recognizes emotions from video taken during treatment, showing a positive impact that could help motivate physiotherapy patients, improving their motivation and recovery.

A realização de atividades de teste é indispensável para a garantia da qualidade de um produto e para a identificação de defeitos, diminuindo custos de manutenção e evitando ao máximo o risco do cliente encontrar esses defeitos. Nessa linha, testes baseados em modelos têm se mostrado atrativos, pois o custo de geração de casos de testes e de correção de defeitos tende a ser menor. Devido à sua simplicidade conceitual e expressividade na descrição do comportamento de um sistema, um dos modelos mais usados e pesquisados na área de teste baseado em modelos são as Máquinas de Estados Finitos (MEFs). Por meio de MEFs e com apoio de ferramentas apropriadas, a geração de casos de testes para avaliar os comportamentos esperados de um sistema é automatizada, reduzindo tanto o custo da geração e da manutenção quanto as falhas humanas. Desta forma, a aplicabilidade de métodos de geração de casos de teste baseados em modelos no contexto de sistemas embarcados vem sendo investigada. O objetivo deste trabalho de mestrado consiste em investigar a aplicabilidade dos métodos de geração em cenários de teste reais, com foco em sistemas embarcados, identificando as difi- culdades e limitações do processo, bem como os requisitos essenciais para a adequação dos métodos de geração propostos na literatura e de ferramentas de apoio à atividade de teste. O foco principal do projeto é a implementação de mecanismos que atendam aos requisitos levantados, visando a usabilidade, segurança e portabilidade da ferramenta / Test activities are essential to ensure the quality of products and identify faults to reduce maintenance costs and avoid that the client finds these faults. In this sense, model-based tests have been proved useful, because the cost of generating test cases and fault correction tend to be smaller. Due to its conceptual simplicity and expressiveness in describing the behavior of a system, Finite State Machines (FSM) have been used and researched in the model-based testing area. FSMs, employed with the support of appropriate tools, enable the generation of test cases in an automated way to assess the expected behavior of a system, reducing both the generation and maintenance costs and human failures. Thus, the applicability of test cases generation methods based on models in the context of embedded systems should be investigated. Test cases generation methods based on FSM are designed to derive test cases from the model. In this context, this work aims to investigate the applicability of generation methods in real-world scenarios, focusing embedded systems. It should identify the difficulties and limitations of the process, as well as the essential requirements for the adequacy of generation methods proposed in the literature and tools to support the test activity. The main focus of the project is the implementation of mechanisms that meet the elicited requirements in order to provide usability, security and tool portability

Os sistemas produtivos (SPs) podem utilizar controladores programáveis (CPs) como dispositivos de realização do controle. Neste contexto, programas de controle executados por estes CPs podem ser desenvolvidos de forma que não estejam em conformidade com as especificações de projeto, o que poderá provocar o surgimento de erros funcionais associados à execução de tais programas de controle, erros estes que podem levar os SPs sob controle a um estado que poderá implicar em acidentes envolvendo equipamentos, pessoas e o meio-ambiente. Esta questão tem motivado o surgimento de diversas abordagens para identificar a existência de erros em programas de controle de CPs, de forma a permitir a correção destes erros e garantir, conseqüentemente, maior confiabilidade operacional. O presente trabalho tem por objetivo identificar a existência de erros em programas de controle baseados em LD (Ladder Diagram). Para isto, propõe-se um procedimento de desenvolvimento de modelos baseados em máquinas de estados finitos estendidas (MEFEs), que são gerados a partir do mapeamento de cada um dos rungs contidos no programa de controle que se deseja identificar erros. Uma vez desenvolvidos os modelos em MEFEs, torna-se possível a utilização de uma ferramenta computacional de verificação, própria para estabelecer se os modelos verificados satisfazem determinadas proposições estabelecidas em lógica temporal. Uma proposição em lógica temporal está relacionada a um estado específico do programa de controle modelado, sendo que o objetivo da verificação é o de estabelecer se a proposição estipulada é atendida ou não. Se um determinado estado específico for, por exemplo, um estado indesejado do programa de controle modelado, e este estado for possível de ser alcançado como resultado do processo de verificação realizado, isto impactará na não conformidade do programa de controle com as especificações comportamentais estipuladas na forma de proposição em lógica temporal, indicando haver, portanto, um erro neste programa de controle modelado. Palavras-chave: Controladores programáveis. Linguagem de programação LD. Modelagem e verificação de máquinas de estados finitos estendidas (MEFEs). / Productive systems (PS) can use programmable logic controllers (PLCs) as the devices of accomplishment of the control. In this context, control programs executed by these PLCs can be developed in a way so that they can be in non-conformity with the project specifications, and this fact may result in functional errors related to the control programs execution. These errors can take the PS under control to a state which can lead into accidents involving equipment, people and the environment. This fact has motivated the appearance of different approaches so as to identify the existence of these errors in PLC control programs so that they can be corrected and assure a greater operational reliability. This work aims at identifying the existence of errors in control programs based on Ladder Diagram (LD). In order to accomplish that, a modeling procedure that generates extended finite state machines (EFSMs) is proposed from the mapping of each one of the rungs in the control program whose errors are to be identified. Once the models based on EFSMs are developed it becomes possible to use a computational verification tool, specifically designed to determine if the verified models fulfill determined propositions established in temporal logic. A proposition in temporal logic is related to a specific state of the modeled control program and the objective of the verification is to establish whether the proposition is fulfilled or not. If a determined specific state, for example, is an unwanted state of the modeled control program and if this state is reachable as a result of the verification process, this will impact in the non-conformity of the control program with the behavior specifications established in a temporal logic proposition, indicating an error in this modeled control program.

Orientador: Arnaldo Vieira Moura / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-16T21:26:35Z (GMT). No. of bitstreams: 1 Pedrosa_LehiltonLelisChaves_M.pdf: 884292 bytes, checksum: e39efddad6809b28790b661469a5cfd2 (MD5) Previous issue date: 2010 / Resumo: Métodos formais são amplamente utilizados para modelar especificações e gerar casos de testes, imprescindíveis para validação de sistemas críticos. As Máquinas de Estados Finitos (MEFs) compõem um dos formalismos adotados, com várias aplicações em testes de sistemas aéreos e espaciais, além de sistemas médicos, entre vários outros. O objetivo de um método de geração automática de casos de testes é obter um conjunto de casos de testes, com o qual é possível verificar se uma dada implementação contém falhas. Um problema importante em métodos de geração de casos de teste com cobertura completa de falhas é o tamanho dos conjuntos de testes, que normalmente é exponencial no número de estados da MEF que está sendo testada. Para minimizar esse problema, diversas abordagens são adotadas, envolvendo melhorias nos métodos existentes, restrições do modelo de falhas e o uso de novas estratégias de teste. Esta dissertação estuda métodos automáticos para geração de casos de testes com cobertura completa de falhas e propõe dois novos métodos, que permitem reduzir o tamanho dos conjuntos de testes gerados. Primeiro, combinamos ideias do método Wp e do método G, visando usufruir as vantagens de ambos e obtendo um novo método, denominado Gp. Em seguida, descrevemos um novo modelo de falhas para sistemas compostos de vários subsistemas, possivelmente com um número alto de estados. Formalizamos tais sistemas, introduzindo o conceito de MEFs combinadas, e apresentamos um novo método de testes, denominado método C. Além disso, propomos uma abordagem de testes incremental, baseada no método C, que torna possível o teste de MEFs com um número arbitrário de estados. Estabelecemos comparações com abordagens tradicionais e mostramos que o uso da estratégia incremental pode gerar conjuntos de testes exponencialmente mais eficientes / Mestrado / Teoria da Computação / Mestre em Ciência da Computação

The field of artificial intelligence has gained much knowledge through the implementation of decision-making systems in video games. One of these systems was the Goal Oriented Action Planning system (GOAP) which directs the behavior of an AI-agent through multiple digital artifacts categorized as goals, actions, and plans. The aim of the thesis is to aid in the understanding and creation of GOAP driven AI-agents in a video game setting to promote research on this topic. The research question of this thesis was about finding out how the GOAP architecture compares to other video game decision-making systems. The theoretical framework introduces the concept of the illusion of intelligence in video games and presents a discussion focused on the different components which make up a GOAP system and other components that support it. Additionally, the theoretical framework explains the need for a comparison between different decision-making systems and explains the social impact of game AI research. The methods section introduces the criteria for the comparison between GOAP and other decision-making systems and presents a comparison process that was driven by a literature review. A GOAP system was designed for this thesis using the unified modeling language and concept maps. It was then implemented using C# code in a free-of-charge game engine called Unity. We present the pseudocode for the implementation of the GOAP system and show that this framework is a modular, customizable, and reusable system that enables AI-agents to create plans from a varied set of actions. Finally, the paper suggests further research within game decision-making AI and emphasizes the importance of game AI research for communities of game developers, hobbyists, and others who could benefit from game AI in their projects.

In the area of Discrete Event Systems (DES), formal verification techniques are important in examining a variety of system properties including controllability and nonblocking. Nonetheless, in reality, most software and hardware practitioners are not proficient in formal methods which holds them back from the formal representation and verification of their systems. Alternatively, it is a common observation that control engineers are typically familiar with Moore synchronous Finite State Machines (FSM) and use them to express their controllers’ behaviour. Taking this into consideration, we devise a generic and structured approach to automatically translate Moore synchronous FSM into timed DES (TDES) supervisors. In this thesis, we describe our FSM-TDES translation method, present a set of algorithms to realize the translation steps and rules, and demonstrate the application and correctness of our translation approach with the help of an example. In order to develop our automatic FSM-TDES translation approach, we exploit the structural similarity created by the sampled-data (SD) supervisory control theory between the two models. To build upon the SD framework, first we address a related issue of disabling the tick event in order to force an eligible prohibitable event in the SD framework. To do this, we introduce a new synchronization operator called the SD synchronous product (||SD), adapt the existing TDES and SD properties, and devise our ||SD setting. We formally verify the controllability and nonblocking properties of our ||SD setting by establishing logical equivalence between the existing SD setting and our ||SD setting. We present algorithms to implement our ||SD setting in the DES research tool, DESpot. The formulation of the ||SD operator provides twofold benefits. First, it simplifies the design logic of the TDES supervisors that are modelled in the SD framework. This results in improving the ease of manually designing SD controllable TDES supervisors, and reduced verification time of the closed-loop system. We demonstrate these benefits by applying our ||SD setting to an example system. Second, it bridges the gap between theoretical supervisors and physical controllers with respect to event forcing. This makes our FSM-TDES translation approach relatively uncomplicated. Our automatic FSM-TDES translation approach enables the designers to obtain a formal representation of their controllers without designing TDES supervisors by hand and without requiring formal methods expertise. Overall, this work should increase the adoption of the SD supervisory control theory in particular, and formal methods in general, in the industry by facilitating software and hardware practitioners in the formal representation and verification of their control systems. / Dissertation / Doctor of Philosophy (PhD)

Les codes source-canal conjoints sont des codes réalisant simultanément une compression de données et une protection du train binaire généré par rapport à d’éventuelles erreurs de transmission. Ces codes sont non-linéaires, comme la plupart des codes de source. Leur intérêt potentiel est d’offrir de bonnes performances en termes de compression et de correction d’erreur pour des longueurs de codes réduites.La performance d’un code de source se mesure par la différence entre l’entropie de la source à compresser et le nombre moyen de bits nécessaire pour coder un symbole de cette source. La performance d’un code de canal se mesure par la distance minimale entre mots de codes ou entre suite de mots de codes, et plus généralement à l’aide du spectre des distances. Les codes classiques disposent d’outils pour évaluer efficacement ces critères de performance. Par ailleurs, la synthèse de bons codes de source ou de bons codes de canal est un domaine largement exploré depuis les travaux de Shannon. Par contre des outils analogues pour des codes source-canal conjoints, tant pour l’évaluation de performance que pour la synthèse de bons codes restaient à développer, même si certaines propositions ont déjà été faites dans le passé.Cette thèse s’intéresse à la famille des codes source-canal conjoints pouvant être décrits par des automates possédant un nombre fini d’états. Les codes quasi-arithmétiques correcteurs d’erreurs et les codes à longueurs variables correcteurs d’erreurs font partie de cette famille. La manière dont un automate peut être obtenu pour un code donné est rappelée.A partir d’un automate, il est possible de construire un graphe produit permettant de décrire toutes les paires de chemins divergeant d'un même état et convergeant vers un autre état. Nous avons montré que grâce à l’algorithme de Dijkstra, il est alors possible d’évaluer la distance libre d’un code conjoint avec une complexité polynomiale.Pour les codes à longueurs variables correcteurs d’erreurs, nous avons proposé des bornes supplémentaires, faciles à évaluer. Ces bornes constituent des extensions des bornes de Plotkin et de Heller aux codes à longueurs variables. Des bornes peuvent également être déduites du graphe produit associé à un code dont seule une partie des mots de codes a été spécifiée.Ces outils pour borner ou évaluer exactement la distance libre d’un code conjoint permettent de réaliser la synthèse de codes ayant des bonnes propriétés de distance pour une redondance donnée ou minimisant la redondance pour une distance libre donnée.Notre approche consiste à organiser la recherche de bons codes source-canal conjoints à l’aide d’arbres. La racine de l’arbre correspond à un code dont aucun bit n’est spécifié, les feuilles à des codes dont tous les bits sont spécifiés, et les nœuds intermédiaires à des codes partiellement spécifiés. Lors d’un déplacement de la racine vers les feuilles de l’arbre, les bornes supérieures sur la distance libre décroissent, tandis que les bornes inférieures croissent. Ceci permet d’appliquer un algorithme de type branch-and-prune pour trouver le code avec la plus grande distance libre, sans avoir à explorer tout l’arbre contenant les codes. L'approche proposée a permis la construction de codes conjoints pour les lettres de l'alphabet. Comparé à un schéma tandem équivalent (code de source suivi d'un code convolutif), les codes obtenus ont des performances comparables (taux de codage, distance libre) tout en étant moins complexes en termes de nombre d’état du décodeur.Plusieurs extensions de ces travaux sont en cours : 1) synthèse de codes à longueurs variables correcteurs d’erreurs formalisé comme un problème de programmation linéaire mixte sur les entiers ; 2) exploration à l’aide d’un algorithme de type A* de l’espace des codes de à longueurs variables correcteur d’erreurs. / Joint source-channel codes are codes simultaneously providing data compression and protection of the generated bitstream from transmission errors. These codes are non-linear, as most source codes. Their potential is to offer good performance in terms of compression and error-correction for reduced code lengths.The performance of a source code is measured by the difference between the entropy of the source to be compressed and the average number of bits needed to encode a symbol of this source. The performance of a channel code is measured by the minimum distance between codewords or sequences of codewords, and more generally with the distance spectrum. The classic codes have tools to effectively evaluate these performance criteria. Furthermore, the design of good source codes or good channel codes is a largely explored since the work of Shannon. But, similar tools for joint source-channel codes, for performances evaluation or for design good codes remained to develop, although some proposals have been made in the past.This thesis focuses on the family of joint source-channel codes that can be described by automata with a finite number of states. Error-correcting quasi-arithmetic codes and error-correcting variable-length codes are part of this family. The way to construct an automaton for a given code is recalled.From an automaton, it is possible to construct a product graph for describing all pairs of paths diverging from some state and converging to the same or another state. We have shown that, using Dijkstra's algorithm, it is possible to evaluate the free distance of a joint code with polynomial complexity. For errors-correcting variable-length codes, we proposed additional bounds that are easy to evaluate. These bounds are extensions of Plotkin and Heller bounds to variable-length codes. Bounds can also be deduced from the product graph associated to a code, in which only a part of code words is specified.These tools to accurately assess or bound the free distance of a joint code allow the design of codes with good distance properties for a given redundancy or minimizing redundancy for a given free distance. Our approach is to organize the search for good joint source-channel codes with trees. The root of the tree corresponds to a code in which no bit is specified, the leaves of codes in which all bits are specified, and the intermediate nodes to partially specified codes. When moving from the root to the leaves of the tree, the upper bound on the free distance decreases, while the lower bound grows. This allows application of an algorithm such as branch-and-prune for finding the code with the largest free distance, without having to explore the whole tree containing the codes.The proposed approach has allowed the construction of joint codes for the letters of the alphabet. Compared to an equivalent tandem scheme (source code followed by a convolutional code), the codes obtained have comparable performance (rate coding, free distance) while being less complex in terms of the number of states of the decoder. Several extensions of this work are in progress: 1) synthesis of error-correcting variable-length codes formalized as a mixed linear programming problem on integers, 2) Explore the search space of error-correcting variable-length codes using an algorithm such as A* algorithm.

SERVICE oriented architecture (SOA) is an architectural style to structure software systems, fostering loose coupling and dynamic integration among the applications. The use of SOA and Web services to develop complex and large business processes demands more formal and systematic testing. In addition, characteristics of this type of software limit the straightforward application of traditional testing techniques. Model-based testing (MBT) is a promising approach to deal with these problems. This dissertation investigates how two modeling techniques, namely Finite State Machine (FSM) and Event Sequence Graph (ESG), can be used to support MBT of service-oriented applications. Both techniques model different aspects and can be applied in a complementary way. Initially, we define an MBT process for service-oriented applications that employs FSMs. Based on previous experience, we propose a model-based approach to test composite services using ESGs. This approach is holistic, once test suites are generated to cover both desired situations (positive testing) and unexpected behaviors (negative testing). Three experimental studies evaluate the proposed approach: (i) a case study, (ii) a cost analysis, and (iii) a study in industry. Testing tools are also presented to support its practical use / A Arquitetura orientada a serviço (SOA) é um estilo arquitetural para estruturar sistemas de software de modo que exista um baixo grau de acoplamento entre as aplicações e essas possam ser facilmente integradas de forma dinâmica. A incorporação de SOA e serviços Web em sistemas que modelam processos de negócios grandes e complexos contribui para a necessidade de testes mais formais e sistemáticos. Além disso, características próprias dessa nova classe de software fazem com que técnicas de teste tradicionais não possam ser diretamente aplicadas. O teste baseado em modelo (TBM) apresenta-se como uma abordagem promissora que busca a resolução desses problemas. Esta tese investiga como duas técnicas de modelagem, Máquina de Estados Finitos (MEF) e Grafo de Sequência de Eventos (GSE), podem ser utilizadas para apoiar o TBM de aplicações orientadas a serviço. Essas técnicas modelam diferentes aspectos e podem ser aplicadas de forma complementar. Inicialmente, é definido um processo de TBM para aplicações orientadas a serviço que emprega MEFs. Com base na experiência adquirida, é proposta uma abordagem baseada em modelo para o teste de serviços compostos usando GSEs. Essa abordagem é holística uma vez que conjuntos de teste são gerados para cobrir tanto situações desejadas (teste positivo) quanto comportamentos inesperados (teste negativo). Três estudos experimentais avaliam a abordagem proposta: (i) um estudo de caso, (ii) uma análise de custo e (ii) um estudo na indústria. Ferramentas de teste também são apresentadas para apoiar o uso prático da abordagem proposta

Made available in DSpace on 2016-12-12T17:38:37Z (GMT). No. of bitstreams: 1 Moacyr Carlos Possan Junior.pdf: 1940795 bytes, checksum: 58824c0ca3ed2180f9e245d34118e117 (MD5) Previous issue date: 2009-12-15 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work presents a new methodology for the modeling of supervisory control systems based on state machines with outputs, obtained from the automata which represent the supervisors found with the usage of the Supervisory Control Theory (SCT) of Discrete Event Systems (DES). Procedures like that are useful to create the documentation which represents the control logic for large scale systems and for the code generation, as well as allows that the documentation and program code updates be easier when new requirements to change the control logic in flexible systems appear. Besides, it makes way for the generation of more reliable solutions and also for the possibility of automatic code generation. The proposed technique consists on the obtaining of finite state machines with outputs using as input information the automata of the supervisors obtained by the SCT and the control actions of the system, where the control logic redundancies existing in the model of the automata are eliminated. Methodologies based on either monolithic or local modular approach are proposed, where the obtained machines are further simplified in order to have simpler models which are used as templates for the implementation in Programmable Logic Controller (PLC) using Ladder language. The methodology is shown using a simple manufacturing system as example to help on its understanding. Besides, this work deals with the difficulties found in the migration from the event based theory in the TCS to the signal based practice for the CLPs. After the presentation of this methodology, it is performed the modeling and implementation for a larger system, a manufacturing cell where a comparison with another existing methodology which also has the SCT as base is performed in order to verify the advantages and disadvantages of such methodology. / Este trabalho apresenta uma nova metodologia para a modelagem de sistemas de controle supervisório baseados em máquinas de estados com saídas, obtidas a partir dos autômatos que representam os supervisores encontrados com o uso da Teoria de Controle Supervisório (TCS) de Sistemas a Eventos Discretos (SEDs). Procedimentos como este são úteis para criar a documentação relativa à especificações de sistemas de grande porte e à geração de código, assim como permitem que a atualização da documentação e do código seja facilitada quando surgem novos requisitos para variação da lógica de controle em sistemas flexíveis. Além disso, isso abre espaço para a geração de soluções mais confiáveis e também para a possibilidade de geração automática de código. A técnica proposta consiste em obter máquinas de estados finitos com saídas usando como informação os autômatos dos supervisores obtidos por intermédio da TCS e as ações de controle do sistema, onde redundâncias da lógica de controle presentes no modelo do autômato são eliminadas. São propostas abordagens tanto no contexto monolítico quanto no contexto modular local, onde as máquinas obtidas são reduzidas posteriormente com o intuito de obter modelos mais simples, que servem como referência para a implementação em Controlador Lógico Programável (CLP) usando linguagem Ladder. A metodologia é demonstrada usando um sistema de manufatura simples como exemplo a fim de facilitar sua compreensão. Além disso, este trabalho trata das dificuldades encontradas na migração da teoria baseada em eventos da TCS na prática baseada em sinais dos CLPs. Após a apresentação da metodologia, é feita a modelagem e implementação para um sistema de maior porte, uma célula de manufatura onde é efetuada uma comparação com uma metodologia já existente que também têm como base a TCS, com o intuito de verificar as vantagens e desvantagens dessa metodologia