Submitted by Marlene Santos Socorro (marsocorro@gmail.com) on 2018-09-17T15:42:46Z No. of bitstreams: 1 TESE MARLENE SOCORRO ARQUIVO UNICO 2017 (1)f (1).pdf: 5023818 bytes, checksum: 07b4252e3db01765125f7950b8dfcc5b (MD5) / Approved for entry into archive by Uillis de Assis Santos (uillis.assis@ufba.br) on 2018-09-28T19:30:22Z (GMT) No. of bitstreams: 1 TESE MARLENE SOCORRO ARQUIVO UNICO 2017 (1)f (1).pdf: 5023818 bytes, checksum: 07b4252e3db01765125f7950b8dfcc5b (MD5) / Made available in DSpace on 2018-09-28T19:30:22Z (GMT). No. of bitstreams: 1 TESE MARLENE SOCORRO ARQUIVO UNICO 2017 (1)f (1).pdf: 5023818 bytes, checksum: 07b4252e3db01765125f7950b8dfcc5b (MD5) / As relações estabelecidas entre ciência, tecnologia e a sociedade têm provocado um amplo debate em torno das responsabilidades do seu desenvolvimento, em benefício do bem-estar da sociedade. Nessa perspectiva, a divulgação científica surge como uma área que discute a necessidade e o direito da população de apropriar-se do saber científico para que possa participar ativamente dos debates e decisões em torno dos temas científicos e tecnológicos. Nesse contexto, o trabalho aqui apresentado discute os rumos da divulgação científica no estado da Bahia, apresentando e analisando projetos e iniciativas de divulgação científica e tecnológica na área das ciências da natureza, nos espaços não formais na região da Baía de Todos os Santos. A pesquisa foi realizada nos municípios que a integram, sendo: Cachoeira, Candeias, Itaparica, Jaguaripe, Madre de Deus, Maragogipe, Salinas da Margarida, Santo Amaro, São Félix, São Francisco do Conde, Saubara, Simões Filho, Vera Cruz, além da capital baiana Salvador. Foram visitados órgãos e organizações de fomento à pesquisa como Secretaria de Educação, Secretaria de Meio Ambiente, Secretaria de Cultura, Secretaria de Planejamento, Secretaria de Bem-Estar Social e organizações não governamentais. O roteiro de entrevista com dezessete questões foi utilizado durante a investigação nos municípios, objetivando conhecer a regularidade das atividades desenvolvidas na perspectiva de divulgar a ciência e a tecnologia para a população. Também foi analisado o público alcançado, além da formação da equipe executora e financiamentos, dentre outras informações. Foram analisados materiais divulgados durante os eventos, documentos disponibilizados na forma impressa e virtual. Foi possível participar de eventos, como: Semana Kirimurê, realizada no município de São Francisco do Conde; a Semana Nacional de Ciência e Tecnologia promovida pela Secretaria de Ciência e Tecnologia do Estado da Bahia (SECTI-BA), em Salvador, especificamente, na Praça da Ciência montada durante o evento; caminhão do Projeto Educar com Energia, no Parque da Cidade em Salvador; palestra promovida pelo Parque Zoológico de Salvador; visitação ao Museu da Energia em Salvador. Após análise de documentos e informações e da participação nos eventos citados, avaliamos que a divulgação da ciência e tecnologia para a população nos municípios investigados é incipiente e, na sua maioria, desenvolvida por órgãos governamentais, com destaque para as Secretarias do Meio Ambiente. As ações detectadas visam envolver a população na solução de problemas ambientais como limpeza de rio, manguezais e reflorestamento. A situação de vulnerabilidade sócioeconômica da população aliada a escassez de recursos dos municípios, favorece ações voltadas para subsistência em detrimento de ações e projetos que visem contribuir na difícil tarefa de levar conhecimento científico e tecnológico para população. Dentre todos os projetos analisados, destacamos o Museu de Energia, levando em consideração sua regularidade e atendimento a um grande público na divulgação de temas voltados a ciência Física. / ABSTRACT TheThe relations established between science, technology, and society have spawned a broad debate about the responsibilities for its development to benefit the well-being of the society. From this perspective, scientific propagation emerges as an area where the necessity and rights of the population to appropriate this knowledge is discussed, so that in this way the population can actively participate in the debates and decisions about technological and scientific issues. Within this context, the work presented here discusses the directions this propagation of science in the state of Bahia is taking, examining and analyzing projects and initiatives for scientific propagation in the area of hard sciences in non-formal spaces in All Saints Bay. Research was preformed in the municipalities which make up the area of All Saints Bay and are: Cachoeira, Candeias, Itaparica, Jaguaripe, Madre de Deus, Maragogipe, Salinas da Margarida, Santo Amaro, São Félix, São Francisco do Conde, Saubara, Simões Filho, Vera Cruz, as well as the Salvador metropolitan area. Departments and organizations that foment research were visited, such as the Education Secretariat, the Planning Secretariat, the Social Welfare Secretariat and NGOs. A questionnaire with 16 items was used during the investigation in the municipalities in order to understand the regularity of activities developed from the perspective of scientific and technology propagation for the population. The public reached was also analyzed and an executive and financial training team was formed. Material publicized during the events and documents available in print and virtually were also analyzed. It was possible to participate in events such as the Kirimurê Week, held in the municipality of São Francisco do Conde; the National Science and Technology Week promoted by the Science and Technology Secretariat of the State of Bahia (SECTI-BA) in Salvador, specifically in the Science Square erected during the event; an activity developed along the path of the Project Educate with Energy in Salvador’s city park; and a lecture put on by the Salvador Zoo; visitation to the Energy Museum in Salvador. After the analysis of documents and information, and participation in the events cited above, we have evaluated that the propagation of science and technology in the municipalities investigated is incipient and are mostly from governmental departments, particularly the Environmental Secretariat. The majority of actions detected aim to involve the population in solving the environmental problems, such as clean-up of the river, the mangroves and reforestation. The vulnerable socio-economic situation of the population, combined with the scarcity of resources in the municipalities favors actions geared towards subsistence in detriment to actions and projects that aim to contribute to the difficult task of bringing scientific and technological information to the population. Among all the projects analyzed, we highlight the Museum of Energy given that it services a large public with information involving physical science.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

Made available in DSpace on 2014-06-11T19:25:29Z (GMT). No. of bitstreams: 0 Previous issue date: 2008-04-03Bitstream added on 2014-06-13T20:27:38Z : No. of bitstreams: 1 bozatski_mf_me_mar.pdf: 850559 bytes, checksum: e97863cf099ca1ae60ffd92574f52040 (MD5) / Procuramos delimitar o âmbito de interação do humano com a realidade a partir da teoria lingüística expressa no Tractatus Logico-Philosophicus e nas Investigações Filosóficas. A partir da identificação deste âmbito ontológico-lingüístico da ação humana, representadas pela tríade agir/sentir/pensar, demonstraremos como a linguagem representa a realidade a partir da afiguração. Através de contextualizações e aproximações das teorias wittgensteinianas com noções filosóficas tradicionais busca-se demonstrar a inovação do método wittgensteiniano e suas possibilidades de aplicação ao exercício filosófico contemporâneo. / We have tried to delimit the ambit of the human's interaction with the reality starting from the linguistic theory expresses in Tractatus Logico-Philosophicus and in the Philosophical Investigations. Starting from the identification of this ontological-linguistic ambit of the human action, represented by the triad to act/to feel/to think, we will demonstrate as the language it represents the reality starting from the representation. Through contextualize and approaches of the Wittgenstein’s theories with the traditional philosophical notions, we aim for to demonstrate the innovation of the Wittgenstein’s method and your application possibilities to the contemporary philosophical exercise.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-06-15T20:18:58Z No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-06-18T19:19:46Z (GMT) No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Made available in DSpace on 2018-06-18T19:19:46Z (GMT). No. of bitstreams: 1 SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) Previous issue date: 2018-02-22 / O uso de Geradores Automáticos de Código para Métodos Formais não apenas minimiza esforços na implementação de Sistemas de Software, como também reduz a chance da existência de erros na execução destes Sistemas. Estas ferramentas, no entanto, podem ter faltas em seus códigos-fonte que causam erros na geração dos Sistemas de Software, e então a verificação de tais ferramentas é encorajada. Esta tese de Doutorado visa criar e desenvolver uma estratégia para verificar JCircus, um Gerador Automático de Código de um amplo sub-conjunto de Circus para Java. O interesse em Circus vem do fato de que ele permite a especificação dos aspectos concorrentes e de estado de um Sistema de maneira direta. A estratégia de verificação consiste nos seguintes passos: (1) extensão da Semântica Operacional de Woodcock e prova de que ela é sólida com respeito à Semântica Denotacional existente de Circus na Teoria Unificada de Programação (UTP), que é um framework que permite prova e unificação entre diferentes teorias; (2) desenvolvimento e implementação de uma estratégia que verifica o refinamento do código gerado por JCircus, através de uma toolchain que engloba um Gerador de Sistema de Transições Rotuladas com Predicado (LPTS) para Circus e um Gerador de Modelos que aceita como entrada (I) o LPTS e (II) o código gerado por JCircus, e gera um modelo em Java Pathfinder que verifica o refinamento do código gerado por JCircus. Através da aplicação do passo (2) combinada com técnicas baseadas em cobertura no código fonte de JCircus, nós visamos aumentar a confiabilidade do código gerado de Circus para Java. / The use of Automatic Code Generators for Formal Methods not only minimizes efforts on the implementation of Software Systems, but also reduces the chance of existing errors on the execution of such Systems. These tools, however, can themselves have faults on their source codes that may cause errors on the generation of Software Systems, and thus verification of such tools is encouraged. This PhD thesis aims at creating and developing a strategy to verify the code generation from the Circus formal method to Java Code. The interest in Circus comes from the fact that it allows the specification of concurrent and state-rich aspects of a System in a straightforward manner. The code generation envisaged to be verified is performed by JCircus, a tool that translates a large subset of Circus to Java code that implements the JCSP API. The strategy of verification consists on the following steps: (1) extension of Woodcock’s Operational Semantics to Circus processes and proof that it is sound with respect to the Denotational Semantics of Circus in the Unifying Theories of Programming (UTP), that is a framework that allows proof and unification of different theories; (2) development and implementation of a strategy that refinement-checks the code generated by JCircus, through a toolchain that encompasses (2.1) a Labelled Predicate Transition System (LPTS) Generator for Circus and (2.2) a Model Generator that inputs (I) a LPTS and (II) the code generated by JCircus, and generates a model (that uses the Java Pathfinder code model-checker) that refinement-checks the code generated by JCircus. Combined with coverage-based techniques on the source code of JCircus, we envisage improving the reliability of the Code Generation from Circus to Java.

Submitted by Maria Medeiros (maria.dilva1@ufcg.edu.br) on 2018-05-22T14:55:43Z No. of bitstreams: 1 ANNE LORAYNE GERÕNIMO SILVA AUGUSTO MOREIRA - DISSERTAÇÃO (PPGCC) 2016.pdf: 843001 bytes, checksum: 3c03d468b4f80d420da1bad90adf7ca0 (MD5) / Made available in DSpace on 2018-05-22T14:55:43Z (GMT). No. of bitstreams: 1 ANNE LORAYNE GERÕNIMO SILVA AUGUSTO MOREIRA - DISSERTAÇÃO (PPGCC) 2016.pdf: 843001 bytes, checksum: 3c03d468b4f80d420da1bad90adf7ca0 (MD5) Previous issue date: 2016 / Capes / O desenvolvimento de sistemas embarcados possibilitou uma forte expansão no número de aplicações dependentes de dispositivos programáveis em áreas tão distintas como automobilística, sistemas financeiros e sistemas médicos. Uma eventual falha em algum desses sistemas pode provocar diferentes graus de danos e prejuízos e, por isso, exige-se um alto grau de confiabilidade em seu funcionamento. O aumento da complexidade dos novos sistemas computacionais e a pressão econômica e busca de novos mercados, concorrem para a busca da redução nos prazos de entrega dos dispositivos programáveis e de seus softwares e sistemas embarcados. Este trabalho apresenta um estudo de caso para a utilização de um método de verificação formal de software aplicado a um sistema computacional de controle de fluxo adaptativo para Gateways Bluetooth Low-Energy utilizados em sistemas de monitoramento remoto de pacientes. Os resultados obtidos neste trabalho confirmam a viabilidade da aplicação do método na verificação formal do software proposto. / The embedded system development had a positive impact on the expansion of applications dependent on programmable devices inside many areas such as automotive industry, financial services, and medical systems. A failure in any of these systems can cause losses and damages on many levels. Therefore, embedded systems require a high level of reliability while operating. The increasing complexity of these new computational systems, the cost-effective pressure, and the new market demand, contribute to reduce the delivery deadlines of the programmable devices, their softwares, and embedded systems. This research presents a case study in which we evaluated the usage of a formal verification method applied to a computational controlling system, with adaptive flow, for Gateway Bluetooth Low Energy used in patient monitoring systems. The results obtained in this study confirm the application feasibility of the formal verification method of the proposed software.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2018-04-11T19:36:14Z No. of bitstreams: 1 ClevertonHentzAntunes_TESE.pdf: 1017090 bytes, checksum: f067305182409e4dcfb731ca7b2c95ca (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-04-12T23:44:18Z (GMT) No. of bitstreams: 1 ClevertonHentzAntunes_TESE.pdf: 1017090 bytes, checksum: f067305182409e4dcfb731ca7b2c95ca (MD5) / Made available in DSpace on 2018-04-12T23:44:18Z (GMT). No. of bitstreams: 1 ClevertonHentzAntunes_TESE.pdf: 1017090 bytes, checksum: f067305182409e4dcfb731ca7b2c95ca (MD5) Previous issue date: 2017-12-15 / O Conselho Nacional de Desenvolvimento Cient?fico e Tecnol?gico - CNPq / Apesar da exist?ncia de v?rias t?cnicas para a gera??o autom?tica de dados de teste baseados em gram?ticas, poucos trabalhos foram propostos no sentido de melhorar os dados de teste gerados aplicando restri??es sem?nticas. Nesse sentido, contribuimos neste trabalho, nesta dire??o para o caso particular do teste de metaprogramas, um programa que tem como dado de entrada um outro programa. Atualmente, a alternativa natural para o teste deste tipo de programa ? a t?cnica de testes baseados em gram?ticas. Essa t?cnica de teste pode ser aplicada de maneira relativamente simples, por?m com um custo de gera??o e execu??o do conjunto de testes elevado e uma efetividade baixa. Por outro lado, diversas pesquisas e ferramentas de grupos interessados no desenvolvimento de metaprogramas fazem uso intenso do recurso de casamento de padr?es durante a sua implementa??o e especifica??o. Neste caso, os padr?es oferecem uma fonte de informa??o interessante para a cria??o de testes que s?o sintaticamente v?lidos e tamb?m satisfazem restri??es sem?nticas. Dada a limita??o dos testes baseados em gram?ticas e considerando a informa??o embutida nos padr?es existentes nos metaprogramas, temos a oportunidade de contribuir para a melhoria do processo de teste para esses programas. Logo, o objetivo deste trabalho ? avaliar o uso da informa??o de padr?es para o teste de metaprogramas e com isso contribuir no seu processo de teste. No intuito de sistematizar o processo de teste de software, o documento apresenta um processo de design de teste e tamb?m uma fam?lia de crit?rios de cobertura baseados em padr?es para o teste eficiente e sistematizado de metaprogramas baseados em padr?es. S?o propostos quatro crit?rios de cobertura baseados em padr?es e nos crit?rios de particionamento do espa?o de entrada. Tamb?m ? apresentada uma hierarquia entre os crit?rios propostos. Com isso, diferentes n?veis de rigor podem ser requeridos no processo atrav?s da escolha do crit?rio adequado. A valida??o dessas contribui??es ? feita atrav?s de um estudo de caso e uma valida??o emp?rica. O estudo de caso apresenta uma instancia??o de refer?ncia para o processo de design de testes de um verificador de tipos implementado como metaprograma baseado em padr?es. O verificador de tipos ? testado usando um conjunto de testes gerados pelos crit?rios de cobertura baseados em padr?es. A qualidade desse conjunto ? avaliada utilizando a t?cnica de muta??o e atrav?s da compara??o dos resultados obtidos com testes gerados por crit?rios baseados em gram?ticas. Os estudos experimentais indicam a efetividade da aplica??o dos crit?rios baseados em padr?es e o ganho em custo-benef?cio em rela??o aos crit?rios baseados em gram?ticas no contexto do teste de metaprogramas baseados em padr?es. / Although there are several techniques for the automatic generation of test data based on grammars, few studies have been proposed to improve the test data generated by applying semantic restrictions. In this sense, we intend to contribute in this direction for the particular case of testing metaprograms, programs that have other programs as input. Currently, the natural alternative to testing this kind of program is using the grammar-based testing. That testing technique can be applied relatively easily, but with high costs, related to the generation and execution of the test set, and low effectiveness. Many researches and tools dedicated to the development of metaprograms make heavy use of pattern matching for their implementation and specification. In this case, the patterns offer an interesting source of information for creating tests that are syntactically valid and also satisfy semantic constraints. Given the limitation of grammar-based testing and pattern information on the metaprograms, we identified an opportunity to contribute to the improvement of the testing process for these programs. Therefore, the goal of this work is to evaluate the use of pattern information for the testing of pattern-based metaprograms and thus contribute to their testing process. In order to systematize the software testing process, a family of coverage criteria based on patterns is proposed to test pattern-based metaprograms efficiently and systematically. Four pattern-based coverage criteria are proposed, they are based on classical input space partitioning combination criteria. Furthermore, a hierarchical relationship between the criteria is presented. Therefore, different levels of rigor can be required by choosing the appropriate criterion. The validation of these contributions is made using a case study and empirical validation. The case study presents a reference instantiation for the test design process applied to a type checker implemented as metaprogram based on patterns. The type checker is tested using a test set generated by the pattern-based coverage criteria, and the quality of this set is evaluated using the mutation technique. The results obtained are compared with those produced by a test set generated by the grammar-based criteria. The experimental studies indicate the effectiveness of the application of these patternbased criteria and a gain of cost-return in relation to the grammar-based coverage criteria.

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.

As técnicas de teste podem ser divididas, num primeiro nível, naquelas baseadas no código (caixa branca) e naquelas baseadas na especificação (caixa preta ou funcionais). Nenhuma delas é completa pois visam a identificar tipos diferentes de defeitos e a sua utilização em conjunto pode elevar o nível de confiabilidade das aplicações. Assim, tornam-se importantes estudos que contribuam para um melhor entendimento da relação existente entre técnicas funcionais e estruturais, como elas se complementam e como podem ser utilizadas em conjunto. Este trabalho está inserido no contexto do projeto PLAVIS (Plataforma para Validação e Integração de Software em Aplicações Espaciais), e tem como objetivo realizar um estudo comparativo entre as técnicas de geração de casos de teste funcionais (baseadas nas especificações formais) e os critérios estruturais baseados em fluxo de controle e fluxo de dados, aplicados nas implementações. Num contexto específico, esse estudo deve fornecer dados de como se relacionam essas duas técnicas (funcional e estrutural) gerando subsídios para sua utilização em conjunto. Num contexto mais amplo - o do projeto PLAVIS - visa a estabelecer uma estratégia de teste baseada em critérios funcionais e estruturais e que possam, juntamente com as ferramentas que dão suporte a eles, compor um ambiente de teste disponível à utilização em aplicações espaciais dentro do INPE / Testing techniques can be divided, in high level, in code-based ones (white box) and specification based ones (black box). None of them are complete as they intend to identify different kinds of faults. The use of them together can increase the application confidence level. Thus, it is important to investigate the relationship between structural testing techniques and functional testing techniques, how they complete themselves and how they can be used together. This paper was developed in the context of the Plavis (PLAtform of software Validation & Integration on Space systems) project. This project provides comparative studies between functional generation testing techniques (based on formal specifications) and structural generation testing techniques, such as control-flow and data-flow criteria, applied in the implementation. In a specific context, this study provides data about the relationship between these techniques and how they can be used together. In the context of the Plavis project, the goal is to provide a testing strategy, based on functional and structural criteria, and a set of tools, composing a testing environment to be used in Space Applications projects, at INPE

A adoção em larga escala de redes de computadores e gerenciadores de banco de dados contribuiu para o surgimento de sistemas de informação complexos. Atualmente, estes sistemas tornaram-se elementos essenciais na vida das pessoas, dando suporte a processos de negócio e serviços corporativos indispensáveis à sociedade, como automação bancária e telefonia. A utilização de componentes na estruturação destes sistemas promove maior qualidade e flexibilidade ao produto e agiliza o processo de desenvolvimento. Entretanto, para que estes benefícios sejam totalmente observados, é fundamental que os provedores de componentes de prateleira projetem especificações precisas, completas e consistentes. Geralmente, as especificações omitem ou negligenciam o comportamento dos componentes nas situações de falha. Desta forma, a utilização de componentes não confiáveis, cujos comportamentos não podem ser inteiramente previstos, compromete seriamente o projeto de sistemas tolerantes a falhas. Uma estratégia para a especificação de componentes tolerantes a falhas é informar a ocorrência de erros através de exceções e realizar a recuperação dos mesmos por rotinas de tratamento correspondentes. A especificação deve separar claramente o comportamento normal do excepcional, destinado à recuperação do erro. Entretanto, em sistemas concorrentes e distribuídos, a especificação apenas deste tratamento local não é suficiente. Uma exceção pode ser lançada em decorrência de erros sistêmicos (i.e. problemas de rede) que afetam todo o sistema. Assim, determinadas exceções devem ser tratadas em nível arquitetural, envolvendo os demais componentes no tratamento. O modelo conceitual de ações Atômicas Coordenadas (ações CA - Coordinated Atomic actions), bastante aplicado na estruturação de sistemas tolerantes a falhas, define um mecanismo geral para a coordenação do tratamento excepcional dos componentes, que cooperam na execução das atividades e competem por recursos compartilhados. Portanto, o modelo de ações CA oferece uma solução potencialmente viável para a especificação do tratamento de exceções em nível arquitetural. Este trabalho propõe um framework para a especificação do tratamento de exceções em nível arquitetural, baseando-se no modelo de aninhamento de ações CA e utilizando a linguagem orientada a eventos CSP (Communicating Sequential Processes). Sua principal característica é prover um protocolo padronizado para a coordenação do tratamento de exceções, que envolve a cooperação dos componentes do sistema. Além disso, é apresentada uma estratégia para a verificação formal dos sistemas na ferramenta FDR (Failure Divergence Refinement), com base no modelo de refinamento por rastros. / The widespread scale adoption of computer networks and database management systems has contributed to the arising of complex information systems. Nowadays, these systems have become essential aspects in the everyday life, supporting business processes and indispensable enterprise services to society such as banking automation and telephony. The usage of components in structuring of these systems promotes higher quality and flexibility to the product and accelerates the software development process. However, in order to fully observe the benefits it is essential that the suppliers of these COTS (commercial off-the-shelf) design precise, complete and consistent specifications. Generally, the specifications omit or neglect the behavior of these components in exceptional situations. Therefore, the usage of untrustworthy components whose behavior cannot be entirely foreseen seriously compromise the design of fault-tolerant systems. One of the strategies used for the specification of fault-tolerant components is to inform the occurrence of errors through exceptions and make its recovering by the correspondent exception handling routines. The specification should separate clearly the normal behavior from the exceptional one, specially designed for error recovery. However, in concurrent and distributed systems, specification of local exception handling is not enough. An exception could be raised as a result of systemic errors (i.e. network errors) which affect the entire system, thus specific types of exceptions should be treated at an architectural level involving all the other components in this handling activity. The conceptual model of Coordinated Atomic (CA) actions, often applied in the structuring of fault-tolerant systems, defines a general mechanism for coordination of exception handling with components that cooperate while executing activities and compete for shared resources. Therefore, the model of CA actions offers a perfectly viable solution for the specification of exception handling at an architectural level. This work proposes a framework for the specification of exception handling at an architectural level, based on the nesting model of CA actions and using the event-oriented language CSP (Communicating Sequential Processes). Its main characteristic is to provide a standardized protocol for coordination of exception handling that involves the cooperation of system components. Moreover, it is presented a formal strategy for system verification using the FDR (Failure Divergence Refinement) tool, based on the traces refinement model.