Hoje, diante das contínuas mudanças e do mercado competitivo, as empresas e organizações têm sempre a necessidade de adaptar suas práticas de negócios para atender às diferentes exigências de seus clientes e manter-se em vantagem com relação às suas concorrentes. Para ajudá-las a atingir esta meta, uma proposta promissora é o Desenvolvimento Baseado em Componentes (DBC), cuja ideia básica é a de que um novo software possa ser construído rapidamente a partir de componentes pré-existentes. Entretanto, a montagem de sistemas corporativos mais confiáveis e tolerantes a falhas a partir da integração de componentes tem-se mostrado uma tarefa relativamente complexa. E a necessidade de garantir que tal integração não falhe tornou-se algo imprescindível, sobretudo porque as consequências de uma falha podem ser extremamente graves. Para que haja uma certa garantia de que o software seja tolerante a falhas, devem ser realizadas atividades de testes e verificação formal de programas. Isto porque ambas, em conjunto, procuram garantir ao desenvolvedor que o sistema resultante da integração é, de fato, confiável. Mas a viabilidade prática de execução destas atividades depende de ferramentas que auxiliem sua realização, uma vez que a execução de ambas constitui um alto custo para o desenvolvimento do software. Tendo em vista esta necessidade de facilitar a realização de testes e verificação nos sistemas baseados em componentes (DBC), este trabalho de Mestrado se propõe a desenvolver um ambiente integrado para a verificação e teste de protocolos para a coordenação do comportamento excepcional de componentes. / Nowadays, because of continuous changes and the competitive market, companies and organizations have the necessity to adapt their business practices in order to satisfy the different requirements of their customers and then, keep themselves in advantage among their competitors. To help them to reach this aim, a promising purpose is the Component-Based Development (CBD), whose basic idea is that a new software can be built in a fast way from preexisting components. However, mounting more reliable and fault-tolerant corporative systems from components integration is a relatively complex task. And the need to assure that such integration does not fail becomes something essential, especially because the consequences of a failure can be extremely serious. To have a certain guarantee that the software will be fault-tolerant, testing activities and formal verification of programs should be done. This is because both, together, try to assure to developer that the resulting system of the integration is, in fact, reliable. But the practical feasibility of executing these activities depends on tools which support it, once both executions have a high cost to software development. Having the necessity to make test and verification easier in systems based in components (CBD), this work has, as main objective, the development of an integrated environment for verification and test of protocols to the coordination of components exceptional behaviour.

Hoje, diante das contínuas mudanças e do mercado competitivo, as empresas e organizações têm sempre a necessidade de adaptar suas práticas de negócios para atender às diferentes exigências de seus clientes e manter-se em vantagem com relação às suas concorrentes. Para ajudá-las a atingir esta meta, uma proposta promissora é o Desenvolvimento Baseado em Componentes (DBC), cuja ideia básica é a de que um novo software possa ser construído rapidamente a partir de componentes pré-existentes. Entretanto, a montagem de sistemas corporativos mais confiáveis e tolerantes a falhas a partir da integração de componentes tem-se mostrado uma tarefa relativamente complexa. E a necessidade de garantir que tal integração não falhe tornou-se algo imprescindível, sobretudo porque as consequências de uma falha podem ser extremamente graves. Para que haja uma certa garantia de que o software seja tolerante a falhas, devem ser realizadas atividades de testes e verificação formal de programas. Isto porque ambas, em conjunto, procuram garantir ao desenvolvedor que o sistema resultante da integração é, de fato, confiável. Mas a viabilidade prática de execução destas atividades depende de ferramentas que auxiliem sua realização, uma vez que a execução de ambas constitui um alto custo para o desenvolvimento do software. Tendo em vista esta necessidade de facilitar a realização de testes e verificação nos sistemas baseados em componentes (DBC), este trabalho de Mestrado se propõe a desenvolver um ambiente integrado para a verificação e teste de protocolos para a coordenação do comportamento excepcional de componentes. / Nowadays, because of continuous changes and the competitive market, companies and organizations have the necessity to adapt their business practices in order to satisfy the different requirements of their customers and then, keep themselves in advantage among their competitors. To help them to reach this aim, a promising purpose is the Component-Based Development (CBD), whose basic idea is that a new software can be built in a fast way from preexisting components. However, mounting more reliable and fault-tolerant corporative systems from components integration is a relatively complex task. And the need to assure that such integration does not fail becomes something essential, especially because the consequences of a failure can be extremely serious. To have a certain guarantee that the software will be fault-tolerant, testing activities and formal verification of programs should be done. This is because both, together, try to assure to developer that the resulting system of the integration is, in fact, reliable. But the practical feasibility of executing these activities depends on tools which support it, once both executions have a high cost to software development. Having the necessity to make test and verification easier in systems based in components (CBD), this work has, as main objective, the development of an integrated environment for verification and test of protocols to the coordination of components exceptional behaviour.

Submitted by Kleber Silva (kleberbs@ufba.br) on 2017-02-06T17:13:39Z No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-07T12:02:49Z (GMT) No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Made available in DSpace on 2017-02-07T12:02:49Z (GMT). No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Os Agentes Autônomos – AA e os Sistemas Multiagentes – SMA realizam suas tarefas baseados num planejamento e a sua complexidade vai depender de qual ambiente esteja envolvido, principalmente quando este ambiente é dinâmico e não determinista. A verificação de modelos tem sido aplicada para a verificação de propriedades do planejamento de modo a checar a correção de aplicações baseadas em AAs e SMA’s e tal verificação apresenta muitos desafios para contornar situações potenciais de explosão de estados. O futebol de robôs simulados é uma aplicação que apresenta muitas das características e problemas inerentes aos AA’s e SMA’s como um ambiente não determinista e dinâmico, fato este que vem tornando esta aplicação um relevante estudo de caso para a verificação de modelos de SMA’s. O presente trabalho considera a especificação e verificação de planos de um time de futebol de robôs simulado, o qual é baseado na arquitetura multicamada de Agentes Concorrentes(camada cognitiva, camada instintiva, e camada reativa), utilizando o verificador de modelos UPPAAL. Para atingir os objetivos do trabalho foi proposta uma abordagem incremental e evolutiva para modelar e verificar os planos, a qual inclui abstrações e técnicas baseadas em verificação composicional de modelos (Compositional Model Checking), com o objetivo de contornar situações de explosão de estados. O método proposto também pode ser utilizado em aplicações similares, o qual poderia ser suportado por um ambiente computacional interativo para guiar os analistas no processo de verificação de planos de SMA’s com arquitetura multicamada, usando a verificação de modelos.

Tese (Doutorado) - Pontifícia Universidade Católica do Paraná, 2001 / Inclui bibliografias / O problema em verificação automática de assinaturas é, em teoria, um processo de reconhecimento de padrões usado para discriminar as classes de assinaturas originais e as falsas. Apesar dos muitos esforços para desenvolver novas técnicas de verificação de / The problem of signature verification is in theory a pattern recognition task used to discriminate two classes, original and forgery signatures. Even after many efforts in order to develop new verification techniques for static signature verification, the

MENESES FILHO, Juarez de Lima. ArCatch: uma solução para verificação estática de conformidade arquitetural do tratamento de exceção. 2016. 81 f. Dissertação (Mestrado em Ciência da Computação)-Universidade Federal do Ceará, Fortaleza, 2016. / Submitted by Jonatas Martins (jonatasmartins@lia.ufc.br) on 2017-08-16T18:55:49Z No. of bitstreams: 1 2016_dis_jlmenesesfilho.pdf: 1440689 bytes, checksum: b5d68cda9ed0ed25ac65cb0ac5aacb9a (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2017-08-17T11:14:12Z (GMT) No. of bitstreams: 1 2016_dis_jlmenesesfilho.pdf: 1440689 bytes, checksum: b5d68cda9ed0ed25ac65cb0ac5aacb9a (MD5) / Made available in DSpace on 2017-08-17T11:14:12Z (GMT). No. of bitstreams: 1 2016_dis_jlmenesesfilho.pdf: 1440689 bytes, checksum: b5d68cda9ed0ed25ac65cb0ac5aacb9a (MD5) Previous issue date: 2016 / Exception handling is a common error recovery technique employed to improve software robustness. However, studies have reported that exception handling is commonly neglected by developers and is the least understood and documented part of a software project. The lack of documentation and difficulty in understanding the exception handling design can lead developers to violate important design decisions, triggering an erosion process in the exception handling design. Architectural conformance checking provides means to control the architectural erosion by periodically checking if the actual architecture is consistent with the planned one. Nevertheless, available approaches do not provide a proper support for exception handling conformance checking. To fulfill this gap, this work proposes ArCatch: an architectural conformance checking solution to deal with the exception handling design erosion. ArCatch provides: (i) a declarative domain-specific language for expressing design constraints regarding exception handling; and (ii) a design rule checker to automatically verify the exception handling conformance. The usefulness and effectiveness of the approach was evaluated in an evolution scenario composed by 10 versions of an existing web-based Java system. Each version was checked against the same set of exception handling design rules. Based on the results and the feedback given by the system’s software architect, the ArCatch proved useful and effective in the identification of existing exception handling erosion problems and locating its causes in the source code. / O tratamento de exceções é uma técnica de recuperação de erros tipicamente empregada na melhoria da robustez de software. No entanto, estudos recentes relatam que o tratamento de exceção é comumente negligenciado pelos desenvolvedores e é a parte menos compreendida e documentada de um projeto de software. A falta de documentação e a difculdade em compreender o design do tratamento de exceção pode levar os desenvolvedores a violarem decisões de design importantes, desencadeando um processo de erosão no design do tratamento de exceção. A verifcação de conformidade arquitetural fornece meios para controlar a erosão arquitetural, verifcando periodicamente se a arquitetura real mantem-se consistente com a arquitetura planejada. No entanto, as abordagens disponíveis não fornecem um suporte adequado para verificação da conformidade do tratamento de exceção. Para preencher essa lacuna, neste trabalho é proposta ArCatch: uma solução de verificação de conformidade arquitetural para lidar com a erosão do design do tratamento de exceção. ArCatch fornece: (i) uma linguagem específica de domínio declarativa para expressar restrições de design relativas ao tratamento de exceção; e (ii) um verificador de regras de design para verificar automaticamente a conformidade do tratamento de exceção. Foi avaliada a utilidade e a eficácia da abordagem proposta em um cenário de evolução composto por 10 versões de um sistema Java web existente. Cada versão foi verificada contra o mesmo conjunto de regras de design de tratamento de exceção. Com base nos resultados e no feedback fornecido pelo arquiteto de software do sistema, a ArCatch provou ser útil e eficaz na identifcação de problemas de erosão do tratamento de exceção existentes e localizar suas causas no código-fonte.

Made available in DSpace on 2016-08-29T15:33:24Z (GMT). No. of bitstreams: 1 tese_9681_Ata de Defesa.pdf: 637986 bytes, checksum: 049a7d2723e6d0c1208ad9aad2eb9d0d (MD5) Previous issue date: 2016-03-28 / Um dos problemas clássicos da Teoria de Grafos é o problema de isomorfismo de grafos. Esse problema trata de determinar se, dado dois grafos, é possível definir um mapeamento entre seus vértices de forma que sejam respeitadas as conexões definidas por suas arestas. Um algoritmo proposto recentemente para resolver esse problema é o IVL (Iterated Vertex Labelling) [Baroni (2012)]. O GROOVE (GRaph-based Object-Oriented VErification) é uma ferramenta de verificação de modelos baseados em grafos que faz uso de algoritmos de isomorfismo. No contexto do GROOVE, o problema de isomorfismo de grafos se apresenta de uma maneira diferente do problema clássico: não se deseja determinar se dois grafos são isomorfos, e sim se, dado um grafo, ele é isomorfo a algum dos elementos de um conjunto de grafos. Neste trabalho, propõe-se a adaptação do IVL para o GROOVE e a realiza- ção de experimentos computacionais com o objetivo de determinar se essa adaptação traz ganhos de performance para a ferramenta. Os resultados levam à conclusão de que o IVL tem desempenho análogo ao algoritmo de isomorfismos que já está implementado no GROOVE. Além desses resultados, foi investigado em um cenário similar o uso de filtros de não-isomorfismo, com a intenção de determinar o não-isomorfismo entre dois grafos a um custo computacional baixo. Os resultados dos testes indicam que essa abordagem é bastante promissora, sendo capaz de detectar não-isomorfismos com eficiência de quase 100% , com tempos de execução bem mais baixos que os performados pelo algoritmo atual do GROOVE quando executado nesse cenário adaptado. / The graph isomorphism is a classical problem in Graph Theory, which consists of determining if, given two graphs, it is possible to define a mapping between their vertexes in a way so that the connection defined by their edges are respected. An algorithm proposed recently to solve this problem is the IVL (Iterated Vertex Labelling) [Baroni (2012)]. GROOVE (GRaph-based Object-Oriented VErification) is a graph-based model checking tool which makes use of isomorphism algorithms. In GROOVE’s context, the graph isomorphism problem is set differently from the classical problem: they are not interested on determining if two graphs are isomorphic, instead, they want to determine if, given a graph, it is isomorphic to one of the elements of a graph set. In this work, it’s proposed the IVL adaptation to GROOVE and computational experiments in order to test if this new adapted algorithm brings performance gains to the tool. It can be concluded from the results that IVL has a similar performance compared to the current implementation in GROOVE. Beyond those results, it was investigated in a similar framework the use of non-isomorphism filters, intending to determine the non-isomorphism between two graphs in a low computational cost. The test results point out that this is a promising approach, being able to detect non-isomorphisms with almost 100% efficiency, with a much lower running time when compared to current GROOVE algorithm when executed in this framework.

Dissertação (mestrado)—Universidade de Brasília, Faculdade de Tecnologia, Departamento de Engenharia Elétrica, 2017. / Submitted by Robson Amaral (robsonamaral@bce.unb.br) on 2018-05-04T20:22:36Z No. of bitstreams: 1 2017_ÂngelaMariaCristinaClara.pdf: 1286296 bytes, checksum: c3a9837a8e814d6b458fe9609db8cf23 (MD5) / Approved for entry into archive by Raquel Viana (raquelviana@bce.unb.br) on 2018-06-06T19:47:57Z (GMT) No. of bitstreams: 1 2017_ÂngelaMariaCristinaClara.pdf: 1286296 bytes, checksum: c3a9837a8e814d6b458fe9609db8cf23 (MD5) / Made available in DSpace on 2018-06-06T19:47:57Z (GMT). No. of bitstreams: 1 2017_ÂngelaMariaCristinaClara.pdf: 1286296 bytes, checksum: c3a9837a8e814d6b458fe9609db8cf23 (MD5) Previous issue date: 2018-06-06 / Diferentes pesquisas indicam que as empresas que possuem bons modelos de governança de TI apresentam resultados superiores em relação aos concorrentes, especialmente porque executam, de forma consistente, as melhores decisões para a TI. Este trabalho objetiva a identificação de Elementos que Orientem as Ações de Verificação de Conformidade Regulatória – EVCR´s, visando o aprimoramento e o direcionamento da governança de TI, tendo como base as estruturas, os processos e os mecanismos que possibilitem assegurar a legalidade, a conformidade, como também apoiar nos processos de tomada de decisão da organização. Para validar os elementos identificados como efetivamente geradores da verificação de conformidade regulatória, foi analisada a aplicação de tais elementos em uma empresa pública, prestadora de serviços de TI para todo o governo federal. / Different research indicates that companies that have good IT governance models feature superior results compared to competitors, especially as they perform consistently, the best decisions for IT. This study aims to identify elements that guide regulatory compliance verification activities in order to improve and the direction of IT governance, based on the structures, processes and mechanisms that allow for ensuring the legality, compliance, as well as support the organization's decision-making processes. To validate the elements identified as effectively generators of regulatory compliance check, the application of such elements was analyzed in a public company, a provider of IT services to the entire federal government.

Resumo: Para encontrar defeitos de comunicaçõ entre diferentes partes de um sistema é realizado o teste de integração, no qual cada módulo desenvolvido deve ser integrado e testado com os módulos já existentes. Entretanto, um módulo a ser integrado e testado, pode necessitar de recursos de outro módulo ainda em desenvolvimento, levando a necessidade de se construir um stub. Stubs são simula_c~oes de recursos essenciais para o teste mas que ainda não estão disponíveis. O stub não faz parte do sistema, então a construção de stubs implica em custo adicional. Para minimizar a necessidade de stubs e conseqüentemente reduzir o custo do projeto, várias estratégias para integrar e testar módulos foram propostas. Porém, nenhuma dessas estratégias considera uma característica presente na maioria dos sistemas, que é a modularização. Dado este fato, este trabalho propõe uma estratégia que considera agrupamentos de módulos durante o estabelecimento de ordens para a integração e teste. Esta estratégia é implementada em uma abordagem chamada MECBA-Clu, uma abordagem baseada em algoritmos de otimização multiobjetivos e diferentes medidas de acoplamento para avaliar diversos fatores que inuenciam o custo de construção de stubs. A abordagem MECBA-Clu é avaliada através da condução de um experimento com oito sistemas reais, quatro Orientados a Objetos e quatro Orientados a Aspectos, no qual os três diferentes algoritmos evolutivos multiobjetivos NSGA-II, SPEA2 e PAES foram aplicados. Os resultados apontam que o espaço de busca fica restrito a determinadas áreas em que as soluções podem ser encontradas. Além disso, de acordo com quatro indicadores de qualidade utilizados, observa-se que o algoritmo PAES obteve o melhor resultado, seguido pelo NSGA-II e por fim o SPEA2. Exemplos da utilização da abordagem também são apresentados.

Dissertação (mestrado) - Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010. / Submitted by Allan Wanick Motta (allan_wanick@hotmail.com) on 2011-05-09T17:06:46Z No. of bitstreams: 1 2010_WashingtnLuisRibeirodeCarvalhoSegundo.pdf: 529113 bytes, checksum: 3c74f1ea1498ab7ee05b3f8cca2df3e5 (MD5) / Approved for entry into archive by Patrícia Nunes da Silva(patricia@bce.unb.br) on 2011-05-11T20:45:58Z (GMT) No. of bitstreams: 1 2010_WashingtnLuisRibeirodeCarvalhoSegundo.pdf: 529113 bytes, checksum: 3c74f1ea1498ab7ee05b3f8cca2df3e5 (MD5) / Made available in DSpace on 2011-05-11T20:45:58Z (GMT). No. of bitstreams: 1 2010_WashingtnLuisRibeirodeCarvalhoSegundo.pdf: 529113 bytes, checksum: 3c74f1ea1498ab7ee05b3f8cca2df3e5 (MD5) / O cálculo גex representa uma solução importante dentro da classe de cálculos de substituições explícitas que lidam com “nomes”, em oposição aqueles que codificam suas variáveis por índices. Delia Kesner obteve, através de um conjunto de provas construtivas, demonstrações das importantes propriedades do גex. Dentre elas, destacamos a PSN, isso é, a Preservação da Normalização Forte, cuja demonstração faz uso de uma estratégia de redução perpétua, que permitiu uma caracterização indutiva do conjunto SN גex. Estendemos a especificação em Coq, já realizada para o cálculo ג, de B. Aydemir et al, e que utiliza lógica nominal para construção de princípios de indução e recursão _-estrutural. Dessa forma nossa especificação inclui a substituição explícita (s[x=t]) na gramática de termos. Avançamos definindo os sistemas de reescrita e as relações de redução do גex, e concluímos por formalizar alguns resultados para o cálculo, a saber: a FC (Composição Completa), a SIM (Simulação de um passo da β-redução) e ainda outros que caminham para a formalização da PSN. _______________________________________________________________________________ ABSTRACT / The גex-calculus represents an important solution among all the class of explicit substitutions calculi that deal with "names", as opposed to those that encode variables by indices. Delia Kesner developed the proofs, through a set of constructive ones, of important properties of the _ex calculus. Among them, we highlight the PSN property, that is, the Preservation of Strong Normalization, whose proof uses a perpetual reduction strategy which allowed an inductive characterization of the set SN גex. We extended the specifi cation already done in Coq for the -calculus by B. Aydemir et al, using nominal logic to build principles of ג -structural induction and recursion. In this way our specification includes the explicit substitution (s[x=t]) in the grammar of the terms. We go foward by de_ning the rewriting systems and the reduction relations for the ג ex and we conclude by formalizing some results for this calculus, as follows: The FC (Full Composition), SIM (Simulation of One Step of β -Reduction) and others that go in the direction of the formalization of the PSN.

Made available in DSpace on 2014-06-12T15:52:22Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / A crescente demanda por produtos eletrônicos e a capacidade cada vez maior de integração criaram sistemas extremamente complexos em chips, conhecidos como Systemon- Chip ou SoC. Seguindo em sentido oposto a esta tendência, os prazos (time-to-market) para que estes sistemas sejam construídos vem continuamente sendo reduzidos, obrigando que muito mais funcionalidades sejam implementadas em períodos cada vez menores de tempo. A necessidade de um maior controle de qualidade do produto final demanda a atividade de Verificação Funcional que consiste em utilizar um conjuntos de técnicas para estimular o sistema em busca de falhas. Esta atividade é a extremamente dispendiosa e necessária, consumindo até cerca de 80% do custo final do produto. É neste contexto que se insere este trabalho, propondo uma metodologia de Verificação Funcional chamada IVM que irá fornecer todos os subsídios para garantir a entrega de sistemas de alta qualidade, e ainda atingindo as rígidas restrições temporais impostas pelo mercado. Sendo baseado em metodologias já bastante difundidas e acreditadas, como o OVM e o VeriSC, o IVM definiu uma organização arquitetural e um fluxo de atividades que incorporou as principais características de ambas as abordagens que antes estavam disjuntas. Esta integração de técnicas e conceitos resulta em um fluxo de verificação mais eficiente, permitindo que sistemas atinjam o custo, prazo e qualidade esperados