Manufacturers are increasingly being held responsible for the fate of their products once they reach their end-of-life phase. This research uses a combination of total disassembly time and recyclability to gauge the environmental impact of a product at this stage of its use. Recyclability, or wasted weight, is a function of the material contained by a product’s subassemblies as it is taken apart. This project suggests a graph-based method of representing product assemblies. Unlike many existing representation methods which are used in the field of automated disassembly, the method proposed here takes component connection methods into account. This, combined with a library of disassembly defining graph grammars, ensures that the disassembly simulation performed on this assembly approximates real-life disassembly procedures as closely as possible. The results of this simulation are Pareto sets whose contents represent various points in the disassembly process. Each member of the set is evaluated using the two primary parameters of disassembly time and wasted weight. This Pareto set can be used to judge a particular product’s performance during end-of-life, from the perspective of recyclability, against that of another product. / text

M.S. / Computer Science & Engineering / The Graph Reduction Machine (G-Machine) is an architecture intended to achieve high performance in executing functional language programs. The success or failure of this novel architecture can only be determined by its performance in executing "real" programs. The simulator of the G-Machine, described in this thesis, makes possible detailed studies of the performance of the G-Machine architecture even though the hardware implementation of a G-Machine is not complete.

Esta tese apresenta um modelo conceitual para modelagem e vericação de espe- cificações de sistemas orientados a objeto. Mais especificiamente, uma extensão da abordagem algébrica baseada em single-pushouts para gramáticas de grafos tipadas é desenvolvida, onde os morfismos de tipagem são compatíveis com as relações de ordem sobre os nodos e (hiper)arcos de um grafo, e que representam, respectivamente, as relações de herança entre classes e sobrescrita de métodos. O trabalho é dividido em trÊs linhas principais: especificações de sistemas, comportamento dinâmico de programas, e verificaçaõ formal de sistemas orientados a objeto. A hierarquia de classes de um sistema orientado a objetoé modelada por um hipergrafo rotulado chamado grafo de classes, cujos conjuntos de nodos e arcos possuem uma relação de ordem parcial restrita, com o objetivo de modelar herança e sobrescrita de métodos. Restrições adicionais garantem que grafos de classes provÊm um modelo fiel e adequado da maneira como as classes de um sistema orientado a objetos s~ao efetivamente organizadas e combinadas. Grafos orientados a objeto são hipergrafos tipados sobre um grafo de classes. O morfismo de tipagem exige que hiperarcos mapeados preservem as relações existentes entre os seus nodos de origem e destino. Esta característica modela a heran»ca de forma adequada, visto que qualquer objeto pode fazer uso de atributos ou mensagens herdadas. Mor¯smos entre grafos orientados a objeto asseguram que o polimorfismo de subclasses seja uma característica intrínseca do formalismo aqui apresentado. Regras orientadas a objeto respeitam os princípios de encapsulamento e oclusão da informação do paradigma. Uma derivação direta (ou aplicação de regra)é uma soma amalgamada (pushout) na categoria de grafos orientados a objeto e seus morfismos. Gramáticas de grafos orientados a objeto modelam o comportamento dinâmico de sistemas. Uma semântica observacional para gramáticas de grafos orientados a objeto, baseada em sistemas de transição rotulados, é definida. Tal semântica é baseada na noção de entidades visíveis (objetos ou mensagens), e que representam os elementos importantes no processo de verificação de propriedades do sistema especificado pela gramática. Finalmente, uma tradução formal de gramáticas de grafos orientados a objeto para programas na linguagem Promela é definida. Objetos são traduzidos como pro- cessos em Promela, e a troca de mensagens entre objetos é implementada com canais de comunicação. Herança, polimorfismo e ligação dinÂmica são implementados no programa Promela, que originalmente não suporta nenhuma dessas caraterísticas. A verificação de propriedades do programa pode ser efetuada tanto sobre estados como sobre eventos. / This thesis presents a graph-based formal framework to model and verify object- oriented specifications. More specifically, an extension of the algebraic single- pushout approach to (typed) graph grammars is developed, where the typing mor- phisms are compatible with the order relations defined over nodes and edges to represent, respectively, inheritance and overriding of classes and methods. This work is divided in three main lines: static specifications, dynamic behaviour, and formal verification of object-oriented systems. The object-oriented class hierarchy structure is modeled by a graph structure called class-model graph, whose set of nodes and edges have a restricted partial order relation over them, to model inheritance and method overriding. The underlying relations of such sets obey additional restrictions, intended to assure that class- model graphs provide an adequate and faithful model of how object-oriented classes are organized and combined. Object-oriented graph grammars model the dynamics of object-oriented systems. Object-oriented graphs are hypergraphs typed over a class-model graph, but the typing morphism is more flexible than the traditional one, in the sense that mapped hyperedges need to preserve relations between sources and targets. This feature adequately models inheritance, for any object can make use of inherited attributes or messages. Morphisms between object-oriented graphs assure that subclass poly- morphism is a built-in feature of the formalism. Object-oriented rules respect the principles of encapsulation and information hiding of the object-oriented paradigm. A direct derivation (or rule application) is shown to be a pushout in the category of object-oriented graphs and their morphisms. An observational semantics for object-oriented graph grammars, based on a labeled transition system, is presented. This semantics is based on a notion of visible entities (objects or messages), which are the elements we are interested in for verification purposes. Finally, a formal translation from object-oriented graph grammars specifications into Promela programs is defined. Objects in the system graph are translated as Promela processes, and message exchange is implemented with buffered communication channels. The semantics of grammar rule application is preserved by the nondeterminism in the choice of which message to consume. Inheritance, polymorphism and dynamic binding are implemented in the Promela program, which originally does not support it. The translation presented assures that both state and event verification can be performed.

A área de biologia computacional está vivendo um crescimento rápido causado pela revolução no estudo de genômas e pelo avanço das técnicas de manipulação do material genético. Com essas novas tecnologias para manipulação de seqüências, a importância de achar uma solução eficiente para os problemas chamados de intratáveis também cresceu, pois muitos problemas envolvidos na análise de DNA pertencem a essa classe de problemas. Uma abordagem para achar essas soluções é usar o próprio DNA para realizar computação, aproveitando o paralelismo massivo utilizado em operações que manipulam seqüências de DNA. Isto é estudado na área de computação com DNA. Esse trabalho propõe um modelo formal para representar a estrutura da molécula de DNA e das operações que são realizadas com ela em laboratório. Este modelo ajuda a preencher a necessidade de uma descrição matemática que possa ser usada para analisar algoritmos baseados em DNA, assim como possibilitar a simulaç~o desses algoritmos em um computador. Foi utilizada a teoria de gramáticas de grafos, uma linguagem de especificação formal, para modelar as seqüências de DNA e suas I operações. O trabalho apresenta um estudo da estrutura da molécula de DNA, deScrevendo suas características e as principais operações que são realizadas para sua manipulação em laboratório. Uma descrição da teoria de Gramática de Grafos e sua aplicação também é apresentada. Para validação do modelo proposto as especificações resultantes foram adaptadas para o formato L-systems, outra linguagem de especificação formal, permitindo realizar a simulação da especificação no ambiente L-Studio. / The area of computational biology is living a fast growth, fed with a revolution in the study of genomes and with the advance in the techniques of genetic material manipulation. With these new technologies for manipulation of sequences, the relevance of finding efficient solution to the so-called computer intractable problems has also grown, because many problems involved in analyzing DNA belong to this class of problems. One approach to find such solutions is to use DNA itself to perform computations, taking advantage of the massive parallelism involved in operations that manipulate DNA sequences. This is what is studied in the area ofDNA computing. This work proposes a formal model to represent the DNA structure and the operations performed in laboratory with it. This model helps to fill the need of a mathematical description that can be used to analyze DNA-based algorithms, as well as for simulating such algorithms in a computer. We use graph grammars, a formal specification language, to model the DNA sequences and operations. The work presents a study of the DNA molecule structure, describing its features and the main operations performed for manipulation in laboratory. A description of the theory of Graph Grammars and its application are presented too. To validate the proposed model, the resulting DNA-graph grammar specifications are then translated into the L-systems format, another formal specification language, allowing for the simulation of the specifications using the L-Studio environment.

Esta tese apresenta um modelo conceitual para modelagem e vericação de espe- cificações de sistemas orientados a objeto. Mais especificiamente, uma extensão da abordagem algébrica baseada em single-pushouts para gramáticas de grafos tipadas é desenvolvida, onde os morfismos de tipagem são compatíveis com as relações de ordem sobre os nodos e (hiper)arcos de um grafo, e que representam, respectivamente, as relações de herança entre classes e sobrescrita de métodos. O trabalho é dividido em trÊs linhas principais: especificações de sistemas, comportamento dinâmico de programas, e verificaçaõ formal de sistemas orientados a objeto. A hierarquia de classes de um sistema orientado a objetoé modelada por um hipergrafo rotulado chamado grafo de classes, cujos conjuntos de nodos e arcos possuem uma relação de ordem parcial restrita, com o objetivo de modelar herança e sobrescrita de métodos. Restrições adicionais garantem que grafos de classes provÊm um modelo fiel e adequado da maneira como as classes de um sistema orientado a objetos s~ao efetivamente organizadas e combinadas. Grafos orientados a objeto são hipergrafos tipados sobre um grafo de classes. O morfismo de tipagem exige que hiperarcos mapeados preservem as relações existentes entre os seus nodos de origem e destino. Esta característica modela a heran»ca de forma adequada, visto que qualquer objeto pode fazer uso de atributos ou mensagens herdadas. Mor¯smos entre grafos orientados a objeto asseguram que o polimorfismo de subclasses seja uma característica intrínseca do formalismo aqui apresentado. Regras orientadas a objeto respeitam os princípios de encapsulamento e oclusão da informação do paradigma. Uma derivação direta (ou aplicação de regra)é uma soma amalgamada (pushout) na categoria de grafos orientados a objeto e seus morfismos. Gramáticas de grafos orientados a objeto modelam o comportamento dinâmico de sistemas. Uma semântica observacional para gramáticas de grafos orientados a objeto, baseada em sistemas de transição rotulados, é definida. Tal semântica é baseada na noção de entidades visíveis (objetos ou mensagens), e que representam os elementos importantes no processo de verificação de propriedades do sistema especificado pela gramática. Finalmente, uma tradução formal de gramáticas de grafos orientados a objeto para programas na linguagem Promela é definida. Objetos são traduzidos como pro- cessos em Promela, e a troca de mensagens entre objetos é implementada com canais de comunicação. Herança, polimorfismo e ligação dinÂmica são implementados no programa Promela, que originalmente não suporta nenhuma dessas caraterísticas. A verificação de propriedades do programa pode ser efetuada tanto sobre estados como sobre eventos. / This thesis presents a graph-based formal framework to model and verify object- oriented specifications. More specifically, an extension of the algebraic single- pushout approach to (typed) graph grammars is developed, where the typing mor- phisms are compatible with the order relations defined over nodes and edges to represent, respectively, inheritance and overriding of classes and methods. This work is divided in three main lines: static specifications, dynamic behaviour, and formal verification of object-oriented systems. The object-oriented class hierarchy structure is modeled by a graph structure called class-model graph, whose set of nodes and edges have a restricted partial order relation over them, to model inheritance and method overriding. The underlying relations of such sets obey additional restrictions, intended to assure that class- model graphs provide an adequate and faithful model of how object-oriented classes are organized and combined. Object-oriented graph grammars model the dynamics of object-oriented systems. Object-oriented graphs are hypergraphs typed over a class-model graph, but the typing morphism is more flexible than the traditional one, in the sense that mapped hyperedges need to preserve relations between sources and targets. This feature adequately models inheritance, for any object can make use of inherited attributes or messages. Morphisms between object-oriented graphs assure that subclass poly- morphism is a built-in feature of the formalism. Object-oriented rules respect the principles of encapsulation and information hiding of the object-oriented paradigm. A direct derivation (or rule application) is shown to be a pushout in the category of object-oriented graphs and their morphisms. An observational semantics for object-oriented graph grammars, based on a labeled transition system, is presented. This semantics is based on a notion of visible entities (objects or messages), which are the elements we are interested in for verification purposes. Finally, a formal translation from object-oriented graph grammars specifications into Promela programs is defined. Objects in the system graph are translated as Promela processes, and message exchange is implemented with buffered communication channels. The semantics of grammar rule application is preserved by the nondeterminism in the choice of which message to consume. Inheritance, polymorphism and dynamic binding are implemented in the Promela program, which originally does not support it. The translation presented assures that both state and event verification can be performed.

A área de biologia computacional está vivendo um crescimento rápido causado pela revolução no estudo de genômas e pelo avanço das técnicas de manipulação do material genético. Com essas novas tecnologias para manipulação de seqüências, a importância de achar uma solução eficiente para os problemas chamados de intratáveis também cresceu, pois muitos problemas envolvidos na análise de DNA pertencem a essa classe de problemas. Uma abordagem para achar essas soluções é usar o próprio DNA para realizar computação, aproveitando o paralelismo massivo utilizado em operações que manipulam seqüências de DNA. Isto é estudado na área de computação com DNA. Esse trabalho propõe um modelo formal para representar a estrutura da molécula de DNA e das operações que são realizadas com ela em laboratório. Este modelo ajuda a preencher a necessidade de uma descrição matemática que possa ser usada para analisar algoritmos baseados em DNA, assim como possibilitar a simulaç~o desses algoritmos em um computador. Foi utilizada a teoria de gramáticas de grafos, uma linguagem de especificação formal, para modelar as seqüências de DNA e suas I operações. O trabalho apresenta um estudo da estrutura da molécula de DNA, deScrevendo suas características e as principais operações que são realizadas para sua manipulação em laboratório. Uma descrição da teoria de Gramática de Grafos e sua aplicação também é apresentada. Para validação do modelo proposto as especificações resultantes foram adaptadas para o formato L-systems, outra linguagem de especificação formal, permitindo realizar a simulação da especificação no ambiente L-Studio. / The area of computational biology is living a fast growth, fed with a revolution in the study of genomes and with the advance in the techniques of genetic material manipulation. With these new technologies for manipulation of sequences, the relevance of finding efficient solution to the so-called computer intractable problems has also grown, because many problems involved in analyzing DNA belong to this class of problems. One approach to find such solutions is to use DNA itself to perform computations, taking advantage of the massive parallelism involved in operations that manipulate DNA sequences. This is what is studied in the area ofDNA computing. This work proposes a formal model to represent the DNA structure and the operations performed in laboratory with it. This model helps to fill the need of a mathematical description that can be used to analyze DNA-based algorithms, as well as for simulating such algorithms in a computer. We use graph grammars, a formal specification language, to model the DNA sequences and operations. The work presents a study of the DNA molecule structure, describing its features and the main operations performed for manipulation in laboratory. A description of the theory of Graph Grammars and its application are presented too. To validate the proposed model, the resulting DNA-graph grammar specifications are then translated into the L-systems format, another formal specification language, allowing for the simulation of the specifications using the L-Studio environment.

Esta tese apresenta um modelo conceitual para modelagem e vericação de espe- cificações de sistemas orientados a objeto. Mais especificiamente, uma extensão da abordagem algébrica baseada em single-pushouts para gramáticas de grafos tipadas é desenvolvida, onde os morfismos de tipagem são compatíveis com as relações de ordem sobre os nodos e (hiper)arcos de um grafo, e que representam, respectivamente, as relações de herança entre classes e sobrescrita de métodos. O trabalho é dividido em trÊs linhas principais: especificações de sistemas, comportamento dinâmico de programas, e verificaçaõ formal de sistemas orientados a objeto. A hierarquia de classes de um sistema orientado a objetoé modelada por um hipergrafo rotulado chamado grafo de classes, cujos conjuntos de nodos e arcos possuem uma relação de ordem parcial restrita, com o objetivo de modelar herança e sobrescrita de métodos. Restrições adicionais garantem que grafos de classes provÊm um modelo fiel e adequado da maneira como as classes de um sistema orientado a objetos s~ao efetivamente organizadas e combinadas. Grafos orientados a objeto são hipergrafos tipados sobre um grafo de classes. O morfismo de tipagem exige que hiperarcos mapeados preservem as relações existentes entre os seus nodos de origem e destino. Esta característica modela a heran»ca de forma adequada, visto que qualquer objeto pode fazer uso de atributos ou mensagens herdadas. Mor¯smos entre grafos orientados a objeto asseguram que o polimorfismo de subclasses seja uma característica intrínseca do formalismo aqui apresentado. Regras orientadas a objeto respeitam os princípios de encapsulamento e oclusão da informação do paradigma. Uma derivação direta (ou aplicação de regra)é uma soma amalgamada (pushout) na categoria de grafos orientados a objeto e seus morfismos. Gramáticas de grafos orientados a objeto modelam o comportamento dinâmico de sistemas. Uma semântica observacional para gramáticas de grafos orientados a objeto, baseada em sistemas de transição rotulados, é definida. Tal semântica é baseada na noção de entidades visíveis (objetos ou mensagens), e que representam os elementos importantes no processo de verificação de propriedades do sistema especificado pela gramática. Finalmente, uma tradução formal de gramáticas de grafos orientados a objeto para programas na linguagem Promela é definida. Objetos são traduzidos como pro- cessos em Promela, e a troca de mensagens entre objetos é implementada com canais de comunicação. Herança, polimorfismo e ligação dinÂmica são implementados no programa Promela, que originalmente não suporta nenhuma dessas caraterísticas. A verificação de propriedades do programa pode ser efetuada tanto sobre estados como sobre eventos. / This thesis presents a graph-based formal framework to model and verify object- oriented specifications. More specifically, an extension of the algebraic single- pushout approach to (typed) graph grammars is developed, where the typing mor- phisms are compatible with the order relations defined over nodes and edges to represent, respectively, inheritance and overriding of classes and methods. This work is divided in three main lines: static specifications, dynamic behaviour, and formal verification of object-oriented systems. The object-oriented class hierarchy structure is modeled by a graph structure called class-model graph, whose set of nodes and edges have a restricted partial order relation over them, to model inheritance and method overriding. The underlying relations of such sets obey additional restrictions, intended to assure that class- model graphs provide an adequate and faithful model of how object-oriented classes are organized and combined. Object-oriented graph grammars model the dynamics of object-oriented systems. Object-oriented graphs are hypergraphs typed over a class-model graph, but the typing morphism is more flexible than the traditional one, in the sense that mapped hyperedges need to preserve relations between sources and targets. This feature adequately models inheritance, for any object can make use of inherited attributes or messages. Morphisms between object-oriented graphs assure that subclass poly- morphism is a built-in feature of the formalism. Object-oriented rules respect the principles of encapsulation and information hiding of the object-oriented paradigm. A direct derivation (or rule application) is shown to be a pushout in the category of object-oriented graphs and their morphisms. An observational semantics for object-oriented graph grammars, based on a labeled transition system, is presented. This semantics is based on a notion of visible entities (objects or messages), which are the elements we are interested in for verification purposes. Finally, a formal translation from object-oriented graph grammars specifications into Promela programs is defined. Objects in the system graph are translated as Promela processes, and message exchange is implemented with buffered communication channels. The semantics of grammar rule application is preserved by the nondeterminism in the choice of which message to consume. Inheritance, polymorphism and dynamic binding are implemented in the Promela program, which originally does not support it. The translation presented assures that both state and event verification can be performed.

A área de biologia computacional está vivendo um crescimento rápido causado pela revolução no estudo de genômas e pelo avanço das técnicas de manipulação do material genético. Com essas novas tecnologias para manipulação de seqüências, a importância de achar uma solução eficiente para os problemas chamados de intratáveis também cresceu, pois muitos problemas envolvidos na análise de DNA pertencem a essa classe de problemas. Uma abordagem para achar essas soluções é usar o próprio DNA para realizar computação, aproveitando o paralelismo massivo utilizado em operações que manipulam seqüências de DNA. Isto é estudado na área de computação com DNA. Esse trabalho propõe um modelo formal para representar a estrutura da molécula de DNA e das operações que são realizadas com ela em laboratório. Este modelo ajuda a preencher a necessidade de uma descrição matemática que possa ser usada para analisar algoritmos baseados em DNA, assim como possibilitar a simulaç~o desses algoritmos em um computador. Foi utilizada a teoria de gramáticas de grafos, uma linguagem de especificação formal, para modelar as seqüências de DNA e suas I operações. O trabalho apresenta um estudo da estrutura da molécula de DNA, deScrevendo suas características e as principais operações que são realizadas para sua manipulação em laboratório. Uma descrição da teoria de Gramática de Grafos e sua aplicação também é apresentada. Para validação do modelo proposto as especificações resultantes foram adaptadas para o formato L-systems, outra linguagem de especificação formal, permitindo realizar a simulação da especificação no ambiente L-Studio. / The area of computational biology is living a fast growth, fed with a revolution in the study of genomes and with the advance in the techniques of genetic material manipulation. With these new technologies for manipulation of sequences, the relevance of finding efficient solution to the so-called computer intractable problems has also grown, because many problems involved in analyzing DNA belong to this class of problems. One approach to find such solutions is to use DNA itself to perform computations, taking advantage of the massive parallelism involved in operations that manipulate DNA sequences. This is what is studied in the area ofDNA computing. This work proposes a formal model to represent the DNA structure and the operations performed in laboratory with it. This model helps to fill the need of a mathematical description that can be used to analyze DNA-based algorithms, as well as for simulating such algorithms in a computer. We use graph grammars, a formal specification language, to model the DNA sequences and operations. The work presents a study of the DNA molecule structure, describing its features and the main operations performed for manipulation in laboratory. A description of the theory of Graph Grammars and its application are presented too. To validate the proposed model, the resulting DNA-graph grammar specifications are then translated into the L-systems format, another formal specification language, allowing for the simulation of the specifications using the L-Studio environment.

Submitted by Aline Batista (alinehb.ufpel@gmail.com) on 2018-04-18T14:30:20Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Alex_Bertei.pdf: 2631033 bytes, checksum: 64d9253595f75230a7d83432fb89d6e9 (MD5) / Approved for entry into archive by Aline Batista (alinehb.ufpel@gmail.com) on 2018-04-19T14:42:33Z (GMT) No. of bitstreams: 2 Dissertacao_Alex_Bertei.pdf: 2631033 bytes, checksum: 64d9253595f75230a7d83432fb89d6e9 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-04-19T14:42:41Z (GMT). No. of bitstreams: 2 Dissertacao_Alex_Bertei.pdf: 2631033 bytes, checksum: 64d9253595f75230a7d83432fb89d6e9 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-03-13 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / Com o passar dos dias os sistemas de software e hardware evoluem e ficam cada vez mais complexos e sofisticados. Como consequência especificar esses sistemas se torna uma tarefa difícil e trabalhosa. No sentido de assegurar certas propriedades de um sistema, este deve ser especificado por intermédio de uma linguagem que ofereça métodos de análise. Para realizar essas especificações temos diversas técnicas e metodologias, onde algumas técnicas que são disponíveis no mercado podem gerar resultados diferentes do que o especificado e esperado. Para realizar a correção deste problema, tem-se a necessidade de se utilizar métodos formais para gerar a especificação e verificação de sistemas. Sistemas que utilizam métodos formais são especificados formalmente através de um modelo matemático. Gramática de Grafos é uma linguagem formal bastante propícia para especificar sistemas complexos, é interessante o uso delas, pelo fato de possuírem inúmeras técnicas para a verificação e especificação de sistemas que são representadas nesta linguagem, além do que, elas possuem um layout gráfico, que as torna bastante intuitivas, por isso elas são uma linguagem de fácil entendimento. Gramática de Grafos Fuzzy são obtidas através da generalização das gramáticas de grafos, elas são constituídas por vértices e arestas com valores de pertinência associados, dentro do intervalo 0 e 1. Devido a inexistência de técnicas e ferramentas de análise para gramática de grafos fuzzy, o seu uso ainda é bastante restrito. Uma maneira de permitir a análise de sistemas especificados em gramática de grafos fuzzy é através da extensão das abordagens existentes para gramática de grafos, adicionando os conceitos de pertinência aos componentes dos grafos e para isso foi necessário definir gramáticas de grafos fuzzy tipados. Já existe uma abordagem relacional para gramática de grafos que permite o uso dos provadores de teoremas da ferramenta Rodin, utilizando a linguagem Event-B. Desta forma, a proposta deste trabalho é estender essa abordagem de gramática de grafos adicionando os conceitos fuzzy para permitir utilizar a mesma abordagem para analisar gramática de grafos fuzzy, surgindo assim um método de análise para esse tipo de gramática. / With the passing of days software and hardware systems evolve and become increasingly sophisticated and complex. As a consequence, specifying these systems becomes a difficult and laborious task. In order to ensure certain properties of a system, it must be specified through a language that offers methods of analysis. To realize these specifications we have several techniques and methodologies, where some techniques that are available in the market can generate different results than the specified and expected. To perform the correction of this problem, there is the need of using formal methods for generate the specification and verification systems. Systems that use formal methods are formally specified through a mathematical model. Grammar Graphs is a very suitable to specify complex systems formal language, is interesting to use them because they have innumerable techniques for the verification and specification of systems that are represented in this language, besides that, they have a graphical layout, which makes them very intuitive, so they are an easy-to-understand language. Fuzzy graph grammars are obtained through the generalization of graph grammars, they are constituted by vertices and edges with associated membership values within the interval 0 and 1. Due to the inexistence of techniques and analysis tools for fuzzy graph grammars, its use is still quite restricted. One way to allow the analysis of systems specified in fuzzy graphs grammars is the extension of existing approaches for graphs grammars, adding the concepts of pertinence to the components of graphs and for this it was necessary to define fuzzy graph grammars typed. There is already a relational approach to graph grammar that allows the use of the theorems of the Rodin tool using the language Event-B. In this way, the purpose of this work is to extend this approach of grammars of graphs by adding the fuzzy concepts to allow to use the same approach to analyze fuzzy graphs grammars, thus appearing a method of analysis for this type of grammar.

Vários métodos de especificação procuram realizar a modelagem de sistemas sob três visões: uma visão funcional, que procura apresentar as informações que trafegam entre os diversos componentes do sistema, uma visão de dados, que apresenta as relações entre as estruturas de dados estáticas do sistema e a visão dinâmica, que mostra as transformações que o sistema pode sofrer ao longo do tempo. Alguns modelos procuram integrar mais de uma visão, mas, em geral, os modelos possuem sérias deficiências ao tentarem representar mais de um aspecto do sistema ao mesmo tempo, sendo necessário o apoio de outros métodos. Este trabalho apresenta um método de especificação de sistemas que procura integrar a modelagem de dados com a modelagem funcional e dinâmica utilizando-se, para isso, das Gramáticas de Grafos como método formal de especificação. Sendo um grafo formado por vértices, arestas e rótulos, pode-se facilmente criar uma camada de abstração em que o usuário (em geral responsável pela análise de sistemas) manipule um método de especificação com o qual já convive, agora com uma semântica formal definida. Espera-se, com a aplicação do método, gerar modelos passíveis de prova, não ambíguos e que promovam um incremento de qualidade no sistema gerado. / Several specification methods try to realize system modeling following three visions: the functional vision, which is based on representing the information exchange among the several components of the system; the data vision, which represents the relations among the static data structures of the system; and the dynamic vision, which presents the transformations the system may endure over the time. Some models exist that try to integrate more than one of these visions, but, in general, they suffer from deficiencies when trying to represent more than one aspect of the system at the same time, in which case the use of other methods is necessary. This work presents a novel method of systems specification that attempts to integrate data modeling with functional and dynamic modelings using, for this, Graph Grammars as its formal specification method. A graph, being made of nodes, edges and labels, is appropriate for creating, easily, an abstraction layer in which the user (usually responsible for the system analysis) manipulates a specification method which is known to him, but now with a well defined formal semantics. We hope, by applying this method, to generate provable, unambiguous models which promote an increase in the quality of the generated system.