SALES, Juliano Efson Norberto. Coordenação e reconfiguração dinâmica de componentes em uma plataforma de computação paralela. 2012. 144 f. Dissertação (Mestrado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-11T17:31:37Z No. of bitstreams: 1 2012_dis_jensales.pdf: 3112116 bytes, checksum: e6dad36307eb52f19a718046ca764535 (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-18T15:42:23Z (GMT) No. of bitstreams: 1 2012_dis_jensales.pdf: 3112116 bytes, checksum: e6dad36307eb52f19a718046ca764535 (MD5) / Made available in DSpace on 2016-07-18T15:42:23Z (GMT). No. of bitstreams: 1 2012_dis_jensales.pdf: 3112116 bytes, checksum: e6dad36307eb52f19a718046ca764535 (MD5) Previous issue date: 2012 / Long running applications are very common in High Performance Computing (HPC) domains. During the execution of this kind of application, some improvements or corrections can be identified and applied without making invalid the data that has been processed. In these cases, the ability to make changes in a parallel program during execution is considered useful. Dynamic reconfiguration is the term used to describe this technique, which can be implemented using different alternatives, like architecture description languages (ADL). An ADL allows a the specification of a software based on exogenous conectors to combine and define data types and protocols for orchestrating the interaction between components. This research has the goal of designing an ADL and implementing a configuration interpretation environment for the HPE component-based parallel computing platform. The main purpose of this language is to provide the ability to specify exogenous connectors and support dynamic reconfiguration. Case studies evaluate the performance of the component interpretation developed by the ADL, as well as validate the actions of dynamic reconfiguration. The results are an evidence that the overhead in the interpretation process for realistic problem instances is acceptable, in such a way that, when used wisely, the connectors can be used even in production scenarios. In some cases, the interpretation weight can be disregarded. The reconfiguration experiments are also deemed satisfactory, making the simplicity of the mechanism the major draw of the solution. / Nos domínios da Computação de Alto Desempenho (CAD), são comuns aplicações com tempo de execução de longa duração. Durante a execução de uma aplicação dessa natureza, podem ser identificadas melhorias ou correções nos algoritmos em execução que não invalidam o processamento previamente realizado. Neste cenário, a capacidade de realizar modificações em tempo de execução se mostra de grande utilidade. A esta técnica chamamos reconfiguração dinâmica, a qual, dentre outros meios discutidos ao longo do trabalho, pode ser implementada a partir do uso de linguagens de propósito específico como as linguagens de descrição de arquitetura (ADL). Uma ADL permite a especificação de um sistema de software a partir da construção de conectores exógenos com a função de combinar e definir os formatos de dados e protocolos nas interações de componentes. Este trabalho de pesquisa tem como objeto o projeto de uma ADL e a implementação de um ambiente de interpretação de configuração para a plataforma de componentes paralelos HPE (Hash Programming Environment). Essa linguagem tem como principal propósito oferecer a capacidade de especificar conectores exógenos e suporte à reconfiguração dinâmica. Estudos de caso avaliam o desempenho da interpretação dos componentes desenvolvidos pela ADL, como também validam as operações de reconfiguração dinâmica. Os resultados mostram sobrecarga considerada aceitável no processo de interpretação, para instâncias realísticas de problemas, de forma que, quando utilizado com prudência, os conectores podem ser utilizados até mesmo em cenários de produção. Em alguns casos, o peso da interpretação chega a ser desprezível. Os ensaios de reconfiguração também se mostram satisfatórios para os requisitos apresentados, sendo um dos principais diferencias da solução, a simplicidade de uso do mecanismo.

MARCILON, Thiago Braga. Contratos formais para derivação e verificação de componentes paralelos. 2012. 156 f. Dissertação (Mestrado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-12T18:10:13Z No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-22T12:39:34Z (GMT) No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) / Made available in DSpace on 2016-07-22T12:39:34Z (GMT). No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) Previous issue date: 2012 / The use of cloud computing to offer High Performance Computing (HPC) services has been widely discussed in the academia and industry. In this respect, this dissertation is included in the context of designing a cloud computing platform for the development of component-based parallel computing applications, referred as cloud of components. Many important challenges about using the cloud of components relate to parallel programming, an error-prone task due to synchronization issues, which may lead to abortion and production of incorrect data during execution of applications, and the inefficient use of computational resources. These problems may be very relevant in the case of long running applications with tight timelines to obtain critical results, quite common in the context of HPC. One possible solution to these problems is the formal analysis of the behavior of the components of an application through the cloud services, before their execution. Thus, the users of the components may know if a component can be safely used in their application. In this scenario, formal methods becomes useful. In this dissertation, it is proposed a process for specification and derivation of parallel components implementation for the cloud of components. This process involves the formal specification of the components behavior through contracts described using the Circus formal specification language. Then, through a refinement and translation process, which takes the contract as a start point, one may produce an implementation of a component that may execute on a parallel computing platform. Through this process, it becomes possible to offer guarantees to developers about the components behavior in their applications. To validate the proposed idea, the process is applied to contracts that have been described based on two benchmarks belonging to the NAS Parallel Benchmarks, widely adopted in HPC for evaluate the performance of parallel programming and computing platforms. / A aplicação de nuvens computacionais para oferecer serviços de Computação de Alto Desempenho (CAD) é um assunto bastante discutido no meio acadêmico e industrial. Esta dissertação está inserida no contexto do projeto de uma nuvem computacional para o desenvolvimento e execução de aplicações de CAD baseadas em componentes paralelos, doravante denominada nuvem de componentes. Um dos principais desafios na sua utilização consiste no suporte à programação paralela, tarefa bastante suscetível à erros, pois tais erros podem levar, ao longo do desenvolvimento, a problemas de sincronização de processos, que podem causar abortamento da execução e a produção de dados incorretos, bem como a problemas relacionados ao uso ineficiente dos recursos computacionais. É importante que tais problemas sejam tratados no caso de aplicações de longa duração cujo respeito a um cronograma para obtenção de resultados é crítico, aplicações estas bastante comuns no contexto de CAD. Uma possível solução para tais problemas consiste na verificação do comportamento e das propriedades dos componentes na nuvem, antes que seja feita a sua execução, tornando possível que os usuários dos componentes da nuvem saibam se um componente pode ser utilizado com segurança em sua aplicação. Nesse cenário, o uso de métodos formais surge como uma alternativa atraente. A contribuição desta dissertação consiste em um processo de derivação e verificação de propriedades de componentes na nuvem. Tal processo envolve a especificação formal do comportamento dos componentes por meio de contratos descritos pela linguagem Circus. Então, através de um processo de refinamento e tradução tendo como ponto de partida o contrato, chega-se à implementação de um componente para execução sobre uma plataforma de computação paralela. Através desse processo, torna-se possível oferecer garantias aos desenvolvedores em relação ao comportamento dos componentes no contexto de suas aplicações. Para a prova de conceito, o processo é aplicado sobre a especificação "papel-e-caneta" de dois benchmarks do NAS Parallel Benchmarks, IS e CG, bastante difundidos na área de CAD.

Made available in DSpace on 2014-06-12T15:52:01Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2008 / A integração de métodos formais com notações semi-formais visuais é uma tendência em engenharia de software. Métodos formais apresentam uma semântica precisa e permitem verificação de propriedades. No entanto, não são considerados intuitivos. Por outro lado, notações semi-formais visuais, como UML, são facilmente integradas no processo de desenvolvimento de software. Assim, métodos formais e semi-formais visuais são complementares. CSP e UML-RT são, respectivamente, exemplos de notação formal e diagramática usados para especificar e projetar sistemas concorrentes e distribuídos. CSP é um método formal no qual processos representam unidades comportamentais que se comunicam através de canais de comunicação, utilizando passagem de mensagem. UML-RT é uma extensão conservativa de UML na qual cápsulas são unidades comportamentais que se comunicam através de portas de comunicação. Portas realizam protocolos os quais especificam os sinais que podem ser enviados e recebidos através de uma porta, e a ordem na qual os sinais podem ser comunicados. Em um trabalho anterior, Ferreira apresentou um conjunto de regras que sistematizam o mapeamento de CSP para UML-RT, mas uma prova formal deste mapeamento não foi apresentada. Assim, para garantir consistência no desenvolvimento de sistemas concorrentes e distribuídos utilizando este mapeamento, a prova formal do mesmo é indispensável, uma vez que não faz sentido o esforço dedicado à especificação do sistema em CSP e a verificação de propriedades e refinamentos, se uma ou mais regras de mapeamento estiverem incorretas. No entanto, UMLRT não possui uma semântica formal padrão. Entre outras propostas de semântica formal, Ramos propõe uma semântica para UML-RT utilizando OhCircus (uma combinação de CSP e Z com características adicionais de orientação a objetos) como modelo semântico. Neste trabalho, é proposta uma variação da semântica de Ramos para UML-RT usando CSP como modelo semântico. Com base nesta semântica, é apresentada a prova do mapeamento de CSP para UML-RT, considerando o modelo de falhas e divergências de CSP. Assim, este trabalho consolida a integração de CSP e UML-RT proposta por Ferreira, no desenvolvimento de sistemas críticos, concorrentes e distribuídos. Um resultado interessante foi observar que, estritamente, as regras propostas por Ferreira não preservam a semântica de CSP, essencialmente com relação a aspectos de terminação dos processos

Made available in DSpace on 2014-06-12T15:52:29Z (GMT). No. of bitstreams: 2 arquivo5034_1.pdf: 809628 bytes, checksum: 2ff554a299db1e14396d8f0d82fa4d3d (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / O processo de formalização da ciência política, ocorrido principalmente na segunda metade do século XX, ainda encontra resistência de largas parcelas da comunidade científica dessa área de estudos. O objetivo deste trabalho é expor a utilização da teoria dos jogos (TJ), principal ferramenta metodológica de formalização da ciência política, na produção recente em diversas áreas da ciência política. O período analisado é 2000-2006, com análises sobre nove artigos coletados de periódicos de grande circulação internacional na área da ciência política, como o American Political Science Review, o Journal of Conflict Resolution, British Journal of Political Science e o American Journal of Politics. Os artigos foram concentrados em três áreas principais: Relações Internacionais, Análise Institucional e Estudos Legislativos. Neste trabalho não apenas exponho a multiplicidade de aplicações da TJ na ciência política como também teço considerações acerca dos seus limites explicativos e possibilidades de novas percepções acerca dos eventos estudados. As bases do meu argumento sobre vantagens e desvantagens no uso da TJ estão na sua versatilidade, na interdisciplinaridade crescente da ciência política e no individualismo metodológico

Made available in DSpace on 2014-06-12T15:56:13Z (GMT). No. of bitstreams: 2 arquivo2770_1.pdf: 3435334 bytes, checksum: c4ebc011cd6476e268421539acd59c8c (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Associação para Promoção da Excelência do Software Brasileiro / O gerenciamento e o projeto de sistemas de engenharia complexos é um desafio interessante. A engenharia de sistemas é um campo interdisciplinar da engenharia focado na melhoria da qualidade de projetos de sistemas. Ela encoraja o uso de métodos e ferramentas como simulação, otimização, análise de confiabilidade e análise estatística para aumentar o conhecimento do sistema, frequentemente representado como um conjunto de modelos. Uma enorme variedade de sistemas dinâmicos precisa ser controlada e pode ser modelada usando os princípios da Teoria de Controle, a base da disciplina de engenharia de controle. Em particular, a engenharia de controle objetiva criar leis de controle para o sistema, que são modeladas usando diagramas de bloco (também chamados de diagramas de leis de controle) e validadas/verificadas usando simulação. Entretanto, a maior parte das validações de leis de controle realizadas na indústria é feita usando ferramentas de simulação como o Simulink, e simulações não cobrem todos os comportamentos do modelo. Além disso, não é fácil modelar uma arquitetura complexa na qual redundância e monitoramento são comumente usados para se obter segurança. Neste trabalho, nós apresentamos três principais contribuições: (1) um conjunto de regras de tradução de modelos Simulink para a algebra de processos CSP (Communicating Sequential Processes), incluindo uma infraestrutura para suportar vários blocos discretos de Simulink; (2) uma estratégia para validar a integração de uma proposta de arquitetura com as leis de controle; e (3) a validação de um sistema de controle de voo dos profundores de um avião produzido pela Embraer. Os resultados mostram que a estratégia pode ser aplicada a modelos complexos através do uso das técnicas formais de abstração de dados e verificação de modelos. Ademais, a estratégia proposta aprimora o processo de desenvolvimento padrão (modelo V) seguido pela indústria por encontrar potenciais defeitos em fases de especificação do projeto, reduzindo tempo de desenvolvimento e custos

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2017-08-08T13:40:24Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Dissertação-Transformando-modelos-xscade-em-SCR-Kamila-Serafim.pdf: 1127362 bytes, checksum: cb72514ffcaf617a6573ea197ab446c1 (MD5) / Made available in DSpace on 2017-08-08T13:40:24Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Dissertação-Transformando-modelos-xscade-em-SCR-Kamila-Serafim.pdf: 1127362 bytes, checksum: cb72514ffcaf617a6573ea197ab446c1 (MD5) Previous issue date: 2016-09-08 / A construção de um software para domínios particulares tem de atender normas específicasque impõem o atendimento a fatores como rastreabilidade de requisitos e certificação. Por exemplo, a indústria aeronáutica deve atender à norma DO-178B que estabelece restrições para uso de software de aeronaves, que são considerados sistemas críticos. Para um sistema estar de acordo com essa certificação é necessário ter requisitos formais e código certificado; nesta direção, Andrade (ANDRADE, 2013) usou a notação SCR (Software Cost Reduction) para definição de requisitos e a ferramenta SCADE para modelagem de sistemas críticos, com desenvolvimento de um tradutor de SCR para artefatos xscade. A prática de desenvolvimento de sistema, porém, não está restrita à transição entre requisitos e artefatos de projeto. Modificações realizadas nestes últimos devem também ser refletidas nos requisitos. Neste trabalho desenvolvemos um tradutor de artefatos de modelagem da ferramenta SCADE para SCR. Desta forma podemos gerar especificação de requisitos a partir do código (Engenharia Reversa) e complementamos o trabalho anterior desenvolvido por Andrade (ANDRADE, 2013). Para o desenvolvimento do tradutor, utilizamos a plataforma Spoofax por meio da qual descrevemos a sintaxe do esquema XML utilizado em SCADE e também as regras de tradução tendo como alvo SCR. A validação da tradução teve como ponto de partida o resultado do uso do tradutor desenvolvido por Andrade (ANDRADE, 2013), tendo de gerar como saída a mesma entrada do tradutor desenvolvido por Andrade (ANDRADE, 2013). Além disso, desenvolvemos exemplos para demonstrar que a modificação estrutural, com preservação de semântica, em projetos SCADE, é verificável por meio do uso de testes gerados por meio da ferramenta TTM-TVEC / Building a software for particular domains must attend specific standards that impose attendance to factors such as traceability requirements and the certification issue. For example, the airline industry should meet the DO-178B standard that establishes restrictions on the use of aircraft software, which is considered a critical system. For a system to be in accordance with this certification, one must have formal requirements and certified code. In this direction, Andrade (ANDRADE, 2013) used SCR (Software Cost Reduction) for requirements definition and SCADE for modeling critical systems with development of an artifacts a translator from SCR. However the practice of developing is not restricted to the transition from requirements to design artifacts. Changes made on design should be reflected in the requirements. In this work we developed a translator from SCADE to SCR. In this way we can generate requirements specification from the code (reverse engineering) and complement the previous Andrade (ANDRADE, 2013) thesis. For the translator development, we use the Spoofax platform through which we describe the XML schema syntax used in SCADE and also the translation rules having SCR as the target language. The translation validation had as its starting point the result of the translator developed by Andrade (ANDRADE, 2013), where the output is the same input developed by Andrade(ANDRADE, 2013). Furthermore, examples developed to demonstrate that the structural modification that preserves semantics in SCADE, is verifiable through the use of tests generated by the TTM-TVEC tool.

Orientador: Arnaldo Vieira Moura / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-16T20:14:05Z (GMT). No. of bitstreams: 1 Cabral_GlauberModolo_M.pdf: 1025512 bytes, checksum: 7aaf4d32142384e7200596499be77cca (MD5) Previous issue date: 2010 / Resumo: Métodos formais são ferramentas da Engenharia de Software que empregam formalismos matemáticos na construção de programas. Em geral, são compostos por uma ou mais linguagens de especificação e algumas ferramentas auxiliares. A linguagem de especificação algébrica Common Algebraic Specification Language (Casl) foi concebida para ser a linguagem padrão na área de especificação algébrica. A linguagem HasCasl é a extensão da linguagem Casl responsável por suportar lógica de segunda ordem e possui um subconjunto de sua sintaxe que se assemelha à linguagem de programação Haskell e que pode ser executado. O uso prático de uma linguagem de especificação depende da disponibilidade de uma biblioteca padrão de especificações pré-definidas. Embora Casl possua tal biblioteca, esta não disponibiliza propriedades e tipos de dados de segunda ordem. Esta dissertação descreve a especificação de uma biblioteca para a linguagem HasCasl com funções e tipos de dados de segunda ordem, tendo como referência a biblioteca Prelude da linguagem Haskell. Os tipos de dados especificados incluem o tipo booleano, listas, caracteres e cadeias de caracteres, além de classes e funções presentes na biblioteca Prelude. Uma primeira versão da biblioteca faz uso de tipos de dados com avaliação estrita, devido à complexidade de iniciar o processo de especificação com o uso de tipos com avaliação preguiçosa. Um refinamento posterior da biblioteca incluiu o suporte a tipos de dados com avaliação preguiçosa. A verificação de ambas as versões da biblioteca foi realizada com o uso da ferramenta Hets, responsável por traduzir as especificações escritas na linguagem HasCasl para a linguagem HOL e gerar necessidades de prova verificadas com o auxílio do provador de teoremas Isabelle. Para ilustrar o uso dos tipos de dados especificados foram incluídas algumas especificações de exemplo envolvendo listas e tipos booleanos. Algumas sugestões de extensão à biblioteca são propostas, tais como o suporte à recursão e às estruturas infinitas, além do aperfeiçoamento do suporte a provas relacionadas a especificações importadas da biblioteca da linguagem Casl / Abstract: Formal methods can be used as software engineering tools that employ mathematical formalisms for building and verifying programs. They are usually composed of one or more specification languages and some auxiliary tools. The Common Algebraic Specification Language (Casl) is designed to be the standard language in the area of algebraic specification, taking tecnical elements from other specification languages. The HasCasl language is the extention of the Casl language that is responsible for supporting secondorder logic, which has a subset of its syntax resembling the Haskell programming language. The practical use of a specification language depends on the availability of a standard library of pre-defined specifications. CASL has such a library and its specifications can be imported by specifications developed in HasCasl. However, the library of the Casl language does not provide higer order properties and data types. This dissertation describes the specification of a library for the language HasCasl based on the Prelude library from the Haskell programming language. The library created her provides second-order functions and data types. It does so by specifying data types and functions existing in Haskell language, such as boolean, list, character and string types. The first version of our library uses types with strict evaluation. The second version of the library has been refined to support types with lazy evaluation. Verification of both libraries was performed using the Hets tool, which translates specifications to the HOL language, producing proof needs that were discharged with the help of the Isabelle theorem prover. To illustrate the use of our library, some example specifications using lists and boolean types are included. Some suggestions for extension of the library are proposed, dealing with support for infinite structures and numeric data types / Mestrado / Linguagens de Programação / Mestre em Ciência da Computação

Orientador: Jacques Wainer / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-16T22:50:12Z (GMT). No. of bitstreams: 1 Andre_AmauryBosso_M.pdf: 698462 bytes, checksum: 3a97278e3328845adbb26c7cb448204b (MD5) Previous issue date: 2010 / Resumo: O gerenciamento de workflows é uma realidade atualmente, mas os sistemas atuais carecem de suporte à verificação de correção em modelos de workflow. Este trabalho visa a realização de verificações em processos, objetivando a detecção de erros sintáticos, como a existência de atividades mal modeladas, ou seja, sem condições de entrada ou de saída. É objetivo deste trabalho também a definição de verificações de ordem estrutural, como detectar se o processo de workflow não possui deadlocks (estado em que o processo trava sem possibilidade de progredir), ou verificar se existem atividades mortas no processo (atividades impossíveis de serem executadas), ou se há terminações incompletas, ou seja, transições pendentes após o processo ter atingido seus objetivos. Além de verificações sintáticas e estruturais, é necessário também a realização de verificações semânticas do modelo, ou seja, é importante que os processos possam ser validados quanto a características que dizem respeito à sua organização lógica, a um nível um pouco mais alto de informação do que simplesmente estrutural. Por exemplo, é diretamente impactante na qualidade do modelo de um processo, definir se este possui conflitos ao acesso de recursos. Dessa forma, um processo estruturalmente correto, pode ficar travado em um deadlock, devido à concorrência quanto ao acesso de um recurso comum entre atividades distintas. Além disso, verificações de restrições de custo, por exemplo, também podem inviabilizar um processo. Todas essas verificações são importantes para decidir se um processo de workflow é correto. A maior contribuição deste trabalho, é então a definição de uma modelagem de processos de workflow que possibilite a verificação de problemas sintáticos, estruturais e semânticos, todos em uma única ferramenta, que se mostra escalável para processos reais, além de possibilitar a verificação de questões ad-hoc, específicas de cada instância, como verificar ordenações entre atividades específicas, etc / Abstract: Workflow management is a reality nowadays, but today's systems give very little support to verify correctness in workflow models. This work aims to perform formal verification, with the goal of detecting syntactic errors, like the existence of activities poorly modeled, in other words, activities with no precondition or effect. It is a goal too, the definition of workflows structural verification, as to detect if the process does not have deadlocks (state in which the process is stuck with no possibility of getting any further), or verifying if there are dead activities in the process (activities impossible to be reached), or if exist incomplete terminations, ie, pending transitions after the process reached its objectives. Besides syntactic and structural verifications, it is necessary too, to perform semantic verifications in the process, in other words, it is important to validate the processes in respect to characteristics of its logical organization, in a higher level of information than simply structural verification. For example, it is directly impacting in the quality of the process model the definition if it has resource access conflicts. In this way, a process that is structurally correct, can be stuck in a deadlock, due to the concurrency in the access of a common resource of distinct activities. Besides that, verifications of costs restrictions, for example, can spoil a process. All these verifications are important to decide if a workflow model is correct. The main contribution of this work is the definition of workflow processes modeling that makes it possible to perform syntactic, structural and semantic verifications, all in a unique tool, that is showed to be scalable for real process, and even possible to verify ad-hoc questions, specific to the model, as checking activities ordering, for example / Mestrado / Inteligência Artificial, Verificação e Validação / Mestre em Ciência da Computação

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.