Tese (doutorado) - Universidade Federal de Santa Catarina, Centro de Comunicação e Expressão. Programa de Pós-Graduação em Lingüística. / Made available in DSpace on 2012-10-22T21:18:01Z (GMT). No. of bitstreams: 1 235997.pdf: 4268263 bytes, checksum: 5839362ed6d066cfe1f42751d226c321 (MD5) / Nesta tese examinamos o comportamento fonético-fonológico dos róticos intervocálicos na fala de 20 indivíduos oriundos de Blumenau (SC) e Lages (SC). Em um primeiro momento, testamos a potencial influência do alemão sobre a variedade do PB de Blumenau, contrastando essa com a variedade de Lages. No entanto, o foco principal de nosso interesse recai sobre a gramática individual e a questão da distribuição das variantes fonéticas entre os dois tipos de rótico, o r-simples e o r-duplo, na fala de cada informante. Dentro de uma visão funcional, que concebe a língua como um sistema complexo, emergente e auto-organizador, desenvolvemos a nossa abordagem, que parte de uma conexão próxima entre os domínios lingüísticos da fonética e da fonologia. Como metodologia conseqüente de, e coerente com essa abordagem, procedemos a uma avaliação qualitativa e aberta do material empírico. Através de uma análise auditiva e acústica chegamos a distinguir 9 variantes cuja distribuição entre o r-simples e o r-duplo foram relacionadas a fatores lingüísticos intrínsecos, à freqüência das palavras constituintes do corpus e ao grau de contato individual, no caso dos falantes de Blumenau, com o alemão. Revela-se, no mapeamento das variantes na gramática individual, que existe uma correlação entre os fatores item lexical mais freqüente e classe de palavras, e a escolha de variantes para a realização do r-simples e do r-duplo.

Tese (doutorado) - Universidade Federal de Santa Catarina, Centro de Comunicação e Expressão. Programa de Pós-Graduação em Lingüística. / Made available in DSpace on 2012-10-23T09:52:51Z (GMT). No. of bitstreams: 1 238255.pdf: 1544152 bytes, checksum: e78890a68fe2ec2b87f5eeb185811b07 (MD5) / O valor semântico-discursivo de passado imperfectivo, no português falado em Florianópolis, apresenta duas formas de realização: a forma de pretérito imperfeito do indicativo (IMP) e a forma perifrástica constituída pelo auxiliar estar acompanhado do morfema de pretérito imperfeito do indicativo e verbo principal no gerúndio (PPROG). No domínio da imperfectividade, o passado imperfectivo recobre valores que vão desde o progressivo até o habitual, passando pelo durativo, iterativo e por casos de ambigüidade aspectual (imperfectivo genérico, valor em que a especificidade aspectual não é relevante nem para o falante nem para o ouvinte). O passado imperfectivo é uma função caracterizada temporalmente pela relação de ordenação e sobreposição, e aspectualmente, pela relação de inclusão. Em relação ao tempo, o passado imperfectivo refere-se a uma situação anterior ao momento de fala e simultânea ao ponto de referência, também anterior, daí a noção de passado. E, em relação ao aspecto, o passado imperfectivo refere-se a uma situação cujo intervalo inclui o ponto de referência, o que manifesta o andamento da situação em relação à referência, daí a noção de imperfectividade. Considerando os pressupostos da abordagem evolutiva da língua (Croft, 2000, 2002), que lida com duas noções de mudança lingüística: mudança como inovação (Givón 2001, 2002 e o paradigma funcional da gramaticalização (Hopper e Traugott, 1993, Heine et al., 1991)) e como propagação (Weinreich et al., 1968), a expressão variável do passado imperfectivo na fala de Florianópolis é analisada. O corpus da análise é formado por 36 entrevistas do Banco de Dados VARSUL relativas à cidade de Florianópolis, estratificadas quanto ao sexo, tempo de escolarização e faixa etária dos indivíduos. Foram coletadas 882 ocorrências da função dentro da unidade analítica episódio narrativo, das quais 546 de IMP e 336 de PPROG. Os dados foram categorizados e submetidos à análise estatística (regressão logística com cálculo de desvio da média) em três modelos: a análise geral, a análise que considerou apenas o aspecto durativo e a análise que considerou o aspecto durativo em pares mínimos. Os resultados apontam que, apesar de ambas as formas desempenharem a mesma função semântico-discursiva, funcionando como variantes de uma mesma variável lingüística, existem contextos de recorrência específicos. A forma IMP está relacionada à expressão dos aspectos habitual e iterativo, predicados [- dinâmicos], situações longas, de polaridade negativa e ponto de referência imperfectivo. A forma PPROG está relacionada à expressão do aspecto progressivo, predicados [+ dinâmicos], situações instantâneas e curtas, de polaridade positiva e ponto de referência perfectivo. A polarização entre formas e contextos de recorrência é conseqüência das trajetórias de gramaticalização pelas quais passam as formas IMP e PPROG. Socialmente, a variação na expressão do passado imperfectivo está relacionada com a gradação etária dos informantes. Os resultados dão evidências ao modelo evolutivo da linguagem, e confirmam a hipótese de que a gramaticalização (mudança como inovação) é direcional de variação (mudança como propagação).

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 dissertação explora diversos aspectos relacionados a integração entre ferramentas de edição e entre os documentos por estas gerados durante o processo de desenvolvimento de software. São analisados para esta finalidade os conceitos de Hiperdocumento e Gramática de Atributos. E especificada uma ferramenta que assiste o desenvolvimento de software através do use de um mecanismo baseado em gramática, que facilita o estabelecimento e controle de sequencias de utilização das ferramentas de edição. Na ferramenta, e também empregado o conceito de gramática, em conjunto ao conceito de Dicionário de Dados Ativo, para a reavaliação dinâmica de documentos editados. A ferramenta incorpora ainda mecanismos com o enfoque de hiperdocumentos, o que facilita a inter-conexão de informações contidas nos documentos gerados no processo de produção de software. são apresentadas as características de produtividade e qualidade no desenvolvimento de software e os fatores que as influenciam, analisando especificamente ferramentas CASE e a necessidade de integração destas. São analisados os conceitos de Gramática de Atributos (GA), Editor Dirigido por Sintaxe (EDS) baseados em GA e Gerador de Editores Dirigidos por Sintaxe (GEDS), no contexto da Engenharia de Software. É apresentado um exemplo de utilização de GA para obtenção de integração de controle no desenvolvimento de software. são expostos os conceitos de Hiperdocumento no contexto da Engenharia de Software. E apresentado um exemplo de utilização de Hiperdocumentos para obtenção de integração referencial no desenvolvimento de software. Na construção da ferramenta, três mecanismos com o enfoque de hiperdocumentos são aplicados para abordar a integração referencial: a) um mecanismo de estabelecimento de elos entre informações contidas nos documentos editados; b) um mecanismo de "browser" de elos, que permite a visualização e seguimento de elos estabelecidos; e c) um mecanismo de estabelecimento e seguimento de caminhos de leitura dos documentos gerados. Um protótipo da ferramenta, implementado em Eiffel, e apresentado. Alguns resultados dos experimentos realizados com a ferramenta são expostos. Trabalhos futuros sobre a pesquisa são sugeridos. / This work explores several aspects about integration between development tools and the documents generated by them in the process of software development. The concepts of Hyperdocument and Atribute Grammars are analysed for this meaning. A tool which aids the software development process by using a grammar based mechanism is specified. This mechanism facilitates the establishment and the control of the development tools being used. In this tool, the concept of grammar is also used, added to the concept of Active Data Dictionary, for dynamic revaluat ion of the edited documents. The tool has mechanisms with hyperdocument emphasis, which falicitate the relationship between documents generated in the software production. The productivity and quality features in software development and the factors that influence them are presented, specifically considering CASE tools and their necessity for integration. The concepts of Atributes Grammar (AG), Sintax Driven Editor (SDE) based on AG and SDEs generator (SDEG) are analysed in the context of Software Engineering. It is presented one sample of AG application for getting development software control integration. The concepts of Hyperdocument are exposed in the context of Software Engineering. It is presented one sample of Hyperdocument application for getting development software referential integration. In the tool, three mechanisms with Hiperdocument emphasis are applied to get referential integration: a) a mechanism for links establishment between edited documents informations; b) a mechanism for links browsing, that allows the links visualization and pursuit; c) a mechanism for establishment and pursuit documents reading paths. One Eiffel prototype of the tool is presented. Some results of the tool experiments are exposed. Future works about the research are suggested.

Vias biológicas representam interações entre entidades químicas complexas (proteínas, substratos, metabólitos etc.) que ocorrem no nível molecular das células. A representação e compreensão do comportamento destas vias é o principal alvo de estudos da Biologia Sistêmica. Esta área de estudos envolve a construção de modelos matemáticos que possam simular in silico (computacionalmente) o comportamento destes sistemas biológicos verificados in vivo (experimentalmente). Do ponto de vista computacional é evidente que tais sistemas são complexos para abordar e descrever de modo intuitivo. São necessários modelos com valor preditivo, isto é, que permitam descrever os comportamentos do sistema que são experimentalmente verificáveis. Algumas notações gráficas foram propostas para descrever vias biológicas. Entre elas, os diagramas de processos tem sido amplamente utilizados. Um diagrama de processos é essencialmente um grafo no qual vértices e arestas representam componentes biológicos, e há uma notação gráfica associada com cada elemento. Nesta dissertação propomos uma fundamentação formal para a linguagem dos diagramas de processos definindo a sintaxe usando gramática de grafos. Nós definimos primeiramente um grafo chamado BioProc, descrevendo o meta-modelo dos diagramas de processos. Instâncias do grafo BioProc são portanto diagramas de processos modelando vias biológicas. Para descrever a semântica foi proposta uma tradução algébrica dos grafos BioProc para redes de Petri estocásticas generalizadas (GSPNs) já amplamente utilizadas na modelagem de processos biológicos. O uso de gramática de grafos como formalismo intermediário na tradução habilita a verificação sintática da via com a checagem dos tipos válidos que podem ser definidos para cada reação antes da simulação na rede de Petri e usá-las posteriormente para explorar propriedades estruturais e estocásticas do modelo. Além disso serve como base para a evolução do modelo proposto. Isto é relevante já que modelos frequentemente são construídos incrementalmente para se adaptar a novos requisitos e/ou incluir novas características. / Biological pathways represent interactions between complex chemical entities (proteins, substrates, metabolites, etc.) that occur at the molecular level of cells. The representation and comprehension of biological pathways behavior is the main target of research in the field of Systems Biology. This area investigates the construction of mathematical models that can simulate in silico (computationally) the behavior of biological systems checked in vivo (experimentally). From a computational view point it is clear that such systems are too complex to analyze and describe in an intuitiveway. Models with predictive value are needed, describing the behaviors that are experimentally verifiable. There are some graphical notations to describe biological pathways. Among them, process diagrams have been widely used. A process diagram is essentially a graph in which vertices and edges represent biological components, and there is a graphical notation associated with each element. In this master thesis we give a formal foundation for biological process diagrams, by defining their (concrete and abstract) syntax and semantics using a formalism called graph grammars. We first build a graph called BioProc Graph, describing the meta-model of process diagrams. Instances of this BioProc graph are concrete process diagrams modeling biological pathways. To describe the semantics we proposed a translation of BioProc diagrams to generalized stochastic Petri networks (GSPNs) already widely used in modeling biological processes. The use of graph grammar formalism as a basis for translation enables the syntatic verification to check the valid types that can be defined for each reaction after the simulation of Petri net and before that to explore structural and stochastic properties of the model. In addition it serves as the basis for model evolution proposed. This is relevant because models are often built incrementally to adapt to new requirements and/or include new features.

Este trabalho é um estudo da lateral pós-vocálica no que se refere à sua realização como variante velarizada ou vocalizada, sob a perspectiva variacionista. O corpus utilizado é a fala de vinte e oito indivíduos de quatro regiões representativas de diferentes grupos étnicos existentes no Rio Grande do Sul. São examinadas as variáveis lingüísticas e extralingüísticas envolvidas na variação em estudo, confirmando-se a variável grupo étnico como a que mais favorece a presença das duas variantes. Além disso, apresentam-se as regras de velarização e de vocalização da lateral pós-vocálica em termos de traços fonológicos na linha de Clements e discute-se a posição destas no sistema de acordo com a linha da Fonologia Lexical.

Em contraste aos sistemas transformacionais, sistemas reativos são caracterisados por reagir continuamente a estímulos provinientes seu ambiente. Além da reatividade, se considerarmos que muitas aplicações requerem métodos de especificação que possibilitam descrever a distribuição espacial dos estados, sistemas de transformação de grafos parecem ser uma técnica de especificação bastante adequada. Algumas aplicações com essas características são sistemas móveis e vias biológicas. Além disso, diversas abordagens para especificação de sistemas reativos propõem usar linguagens assíncronas para especificar a comunicação entre componentes e definem mecanismos para descrever um conjunto (ou seqüência) de atividades que são realizadas atomicamente. Porém, pouca atenção tem sido dada à idéia de estender sistemas de transformação de grafos para permitir a especificação de atividades atômicas. Recentemente, inspirada nas idéias das redes de Petri “zero-safe” foi definida uma extensão de sistemas de transformação de grafos (GTS) – denominada GTS transacional (T-GTS) – equipando-os com uma noção de transação. Uma transação, nesta abordagem, descreve um conjunto de ações que são executadas de um modo atômico e é definida através de uma distinção entre os recursos visíveis e invisíveis de um ponto de vista externo, onde os últimos são considerados temporários e “esquecidos” em um nível abstrato. Nesta tese é dada uma fundamentação mais teórica para T-GTSs definindo uma noção de morfismos de implementação T-GTS (associando produções de um sistema com transações de outro) e, usando essa noção, é demonstrada a existência de uma adjunção entre as categorias de GTSs e T-GTSs com morfismos de implementação. Além disso, GTSs transacionais são estendidas com um mecanismo para descrever padrões de interação de sistemas reativos através de relações de dependência incluídas nas produções. A idéia é que um sitema interage com seu ambiente consumindo e criando elementos visíveis para à esse ambiente, uma relação de causalidade. Finalmente, propomos uma noção de refinamento para T-GTSs com relação de dependência caracterizada por uma visão “caixa-devidro”, onde alguns aspectos internos são preservados. Em um nível abstrato, o sistema é especificado por produções que descrevem (de uma maneira atômica) reações completas, onde a relação de dependência determina algumas restrições na estrutura interna dessas reações. Um refinamento de um sistema é definido por um morfismo total de implementação que associa cada produção (abstrata) a uma transação. Assim, o sistema refinado preserva todo o comportamento externo do sistema original e as restrições da estrutura interna determinadas pelas relações de dependência. / Reactive systems, in contrast to transformational systems, are characterised by having to continuously react to stimuli from its environment. If, in addition to reactiveness, we consider that for many applications the specification method should provide a way to describe the spatial distribution of states, graph transformation seems to be a suitable specification technique. Some applications with these characteristics are mobile systems and biological pathways. However, the approaches provided for graph transformations so far are not adequate to explicitly describe interaction patterns. Furthermore, several approaches to specify reactive systems propose to use asynchronous languages to specify communication between components and define mechanisms to describe a set (or sequence) of activities that are performed atomically. However, scarce attention has been devoted to the idea of extending GTSs in order to allow the specification of atomic activities. Inspired by the ideas of zero-safe Petri nets, an extension of graph transformation systems (GTSs) – called transactional GTS (T-GTS) – was defined, equipping them with a transaction notion. A transaction, in this approach, describes a set of actions that are executed in an atomic way and it is defined by distinguishing the resources that are visible or invisible from an external point of view, where the last ones are considered temporary and are forgotten at a more abstract level. In this thesis, we give a more theoretical foundation to T-GTS defining a notion of implementation morphisms between T-GTSs (associating graph productions of a system with transactions of other system) and using this notion we demonstrate the existence of an adjunction between categories of GTSs and T-GTSs with implementation morphisms. Moreover, we extends transactional GTSs with a mechanism to describe interaction patterns of reactive systems, by means of dependency relations included in the graph productions. The idea is that a system interacts with its environment by consuming and creating elements visible to this environment, obeying a causal dependency. Finally, we propose a notion of glass-box refinement for T-GTSs with dependency relations, where some internal aspects are preserved. In an abstract level, the system is specified by productions describing (in an atomic way) complete reactions, where the dependency relations give some constraints on the internal structure of these reactions. A refinement of a system is given by a total implementation morphism, that associates each (abstract) production to a transaction. Hence, the refined system preserves all external behaviour of the original system and the internal constraints given by the dependency relations.

[pt] O teste funcional de software é um desafio enfrentado há muito tempo por desenvolvedores. A complexidade crescente de sistemas computacionais torna esse desafio ainda maior. Uma tendência apontada como possível solução deste problema é o uso de teste baseado em modelos. Inspirada neste paradigma, esta dissertação retrata uma pesquisa sobre o uso de gramáticas como modelos de teste funcional. Modelos gramaticais podem capturar conceitos e comportamentos de um sistema e de seu ambiente usando um nível de abstração de acordo com o objetivo de teste. Eles também podem ser aplicados para descrever casos de teste funcional e guiar a execução de casos de teste gerados num sistema em teste. O resultado desta execução, representado na forma de um veredicto, revela a conformidade do sistema com seus requisitos e especificações. Para explorar o potencial dos modelos gramaticais, este trabalho definiu uma maneira sistemática de gerar e executar massas de teste. Esta solução permitiu a programação de diferentes estratégias de teste. Ela também facilitou a adaptação dos testes a mudanças de requisitos e promoveu o reuso dos testes existentes. Como efeito colateral deste estudo, um processo de teste funcional foi desenvolvido e a arquitetura de apoio aqui introduzida pode ser reutilizada ou estendida por futuras soluções de teste funcional. / [en] Software functional test is a challenge faced by developers for a long time. The growing complexity of computing systems turns this challenge even greater. Model-based testing is a trend pointed out by the academia and the industry as a possible solution to this matter. Inspired by this paradigm, this dissertation depicts a research made on the use of grammars as functional test models. Grammar models can capture concepts and behaviors of a system and its environment at a level of abstraction according to the test goal. They also can be applied to describe functional test cases and guide the execution of the generated test cases against a system under test. The result of this execution, represented as a verdict, reveals the system conformity with its requirements and specifications. In order to explore grammar models potential, this work defined a systematic way to generate and execute a mass of tests. This solution allowed the implementation of different test strategies. It also assisted test adjustment to requirements change and promoted existing tests reuse. As a side-effect of this study, a functional test process was developed and the supporting architecture introduced here may be reused or extended by future functional test solutions.

O crescimento da complexidade e do tamanho dos sistemas computacionais atuais suscitou um aumento na dificuldade de extração e especificação de modelos formais desses sistemas, tornando essa atividade cada vez mais dispendiosa, tanto em tempo quanto em custo. Modelos são utilizados em diversas técnicas da Engenharia de Software, com o intuito de auxiliar em processos que compreendem desde o desenvolvimento de novos softwares, até reconstrução de um sistema a partir de software legado, passando pela realização de manutenção de um software em operação. Portanto, é necessário que essas abstrações sejam confiáveis e representem fielmente o software real. Nesse sentido, a adoção de métodos formais para a construção e análise de modelos computacionais é crescente e motivada, principalmente, pela confiabilidade que os formalismos matemáticos agregam aos modelos. No entanto, a utilização de métodos formais geralmente demanda um alto investimento de recursos humanos e, consequentemente, financeiros, uma vez que a utilização de tais formalismos é condicionada ao estudo profundo de sua fundamentação matemática. Considerando-se a extensa aplicabilidade de modelos em diversas subáreas da Ciência da Computação e as vantagens advindas da utilização de métodos formais para especificar sistemas, é interessante identificar métodos e ferramentas existentes para automatizar os processos de extração e análises de modelos, em conjunto com a adoção de formalismos que possam ser utilizados por profissionais da computação que atuam na indústria de software. Dessa forma, é estimulada nesse trabalho a utilização do formalismo de Gramática de Grafos, um método formal que diferencia-se dos demais por ser intuitivo e possuir uma representação visual gráfica, o que facilita a sua compreensão e não exige um conhecimento avançado sobre o formalismo. Primeiramente, é proposta uma abordagem para a extração de modelos em Gramática de Grafos a partir de código-fonte, extraindo informações de execuções de código Java anotado. Em seguida, é apresentada uma metodologia existente para extração e análise de Gramática de Grafos a partir de Casos de Uso, juntamente com um estudo empírico realizado a fim de validar a metodologia. Por fim, são propostas possíveis verificações adicionais, a fim de extender as análises dessa metodologia. Com isso, busca-se a obtenção de modelos, descritos através do formalismo de grafos, a partir de artefatos criados nos dois pólos do processo de desenvolvimento de software, antes e depois da implementação, no sentido de viabilizar futuras comparações, no contexto de verificação de software. / The growing size and complexity of current computer systems leading to an increase in the difficulty of extraction and specification of formal models of such systems, making it increasingly expensive activity, both in time and in cost. Models are used in various techniques of software engineering in order to assist in processes that range from the development of new software, to rebuild a system from legacy software, passing for performing maintenance of software in operation. Therefore, it is necessary that these abstractions are reliable and faithfully represent the actual software. In this sense, the adoption of formal methods for the construction and analysis of models is growing and motivated mainly by the reliability that the mathematical formalism add to models. However, the use of formal methods generally demands a high investment in human resources and hence financial, since the use of such formalism is conditioned to the deep study of its mathematical foundation. Considering the extensive applicability of models in various subfields of computer science and the benefits arising from the use of formal methods for specifying systems, it is interesting to identify existing methods and tools to automate the process of extracting models, in addition to the adoption of formalism that can be used by computer professionals working in the software industry. Thus, we encourage the use of the Graph Grammar formalism, a formal method that differs from others because it is intuitive and has a graphical visual representation, making it easy to understand and does not require an advanced knowledge of the formalism. First, we propose an approach for extracting models from source code in Graph Grammar, getting information of executions of annotated Java code. Then an existing methodology for extraction and analysis of Graph Grammar from Use Cases is presented, along with an empirical study to validate the methodology. Finally, we propose possible additional checks in order to extend the analysis of this methodology. Thus, this work aims to extract models, described by the formalism of graphs, from artifacts created in the two poles of the software development process, before and after implementation, in order to allow future comparisons, in the context of software verification.