Made available in DSpace on 2014-06-12T15:56:31Z (GMT). No. of bitstreams: 2 arquivo2943_1.pdf: 1753239 bytes, checksum: 9bb54530f2681d310412190da2d1397f (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Esta dissertação oferece contribuições para o problema de verificação de assinaturas off-line através da utilização de diferentes distâncias e classificadores de apenas uma classe. O uso de classificadores de uma classe viabiliza a utilização de apenas assinaturas verdadeiras durante a fase de treinamento do sistema. Isso é vantajoso pois em diversas aplicações reais de verificação de assinaturas existe uma carência de assinaturas falsas em detrimento do número de assinaturas verdadeiras. Esse trabalho também realiza uma comparação entre os resultados dos diferentes classificadores de uma classe escolhidos e de três métodos de extração de características implementados: Shadow Code, Características Periféricas e Diferenciais Periféricas e Elementos Estruturais. Afora isso, foram calculadas cinco distâncias utilizando as características extraídas: dmin, dmax, dcentral , dtemplate e dncentral . Essas distâncias foram normalizadas de forma a tornar o sistema independente de classe. E posteriormente combinadas usando as seguintes regras: produto, média, máximo, mínimo e soma. De forma a avaliar a contribuição de cada etapa no desempenho do sistema, este foi subdividido em quatro arquiteturas. Para isso, partiu-se de uma arquitetura mais simples, e foram sendo adicionadas novas etapas a ela. Dessa forma, foi possível identificar que, dentre as extrações utilizadas neste trabalho, o método Shadow Code obteve um grande destaque. O mesmo pode ser dito para as distâncias dcentral e dncentral , que apresentaram melhores resultados que as demais: dmin, dmax e dtemplate. As combinações das distâncias apresentaram resultados discrepantes, algumas combinações pioraram o desempenho do sistema, enquanto outras provocaram um efeito positivo. Foram utilizadas duas bases de dados: Base de Dados 1 (base de dados de assinaturas desenvolvida em pesquisa anterior) e Base de Dados 2 (base de dados de assinaturas disponibilizada em competição para sistemas de verificação de assinaturas). O melhor resultado geral do sistema, para a Base de Dados 1, e considerando 10% de falsos positivos, foi de 93,37% de verdadeiros positivos para as assinaturas falsas aleatórias, 59,18% para as assinaturas falsas habilidosas e 75,85% usando ambas

Made available in DSpace on 2014-06-12T15:56:33Z (GMT). No. of bitstreams: 2 arquivo2954_1.pdf: 1502003 bytes, checksum: 78d97190e617400e07016f4aa1faac70 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2010 / As soluções de software estão cada dia mais presentes no cotidiano das pessoas, e a preocupação com a qualidade desses sistemas cresceu bastante na última década. A exigência do mercado por qualidade levou ao desenvolvimento de modelos para a melhoria do processo de software como o CMMI - o mais conhecido e utilizado atualmente. Como conseqüência dessa busca por remover o maior número possível de erros antes de entregar o software aos clientes, teve início um movimento de especialização de profissionais nas atividades de teste de software (verificação e validação). Atualmente, muitas organizações possuem, inclusive, equipes especializadas em testar o software. Nesse contexto, o processo de testes passou a receber destaque no ciclo de vida de desenvolvimento e manutenção de sistemas. Embora o CMMI, em suas área de processo de Verificação e Validação, defina um guia para a melhoria das mesmas, ele não fornece informações mais detalhadas sobre boas práticas de testes. Assim, é necessário utilizar modelos voltados, especificamente, à melhoria do processo de testes como o Test Maturity Model Integration-TMMi. Nesse trabalho, o TMMi é apresentado como uma ferramenta para alcançar os objetivos definidos pelo CMMI para as áreas de processo de Verificação e Validação (Ver&Val). A partir da proposição de um mapeamento entre as práticas dos dois modelos, realizou-se um estudo prático no qual o processo de desenvolvimento de software de uma organização foi modificado, utilizando práticas do TMMi, com o objetivo de aumentar a capacidade dos processos de Ver&Val segundo o CMMI. Utilizando a abordagem de Pesquisa ação, além de avaliar a utilização conjunta dos dois modelos, foi possível obter resultados em projetos reais da indústria e promover a transferência de conhecimento entre o pesquisador e profissionais

Made available in DSpace on 2014-06-12T15:59:45Z (GMT). No. of bitstreams: 2 arquivo5536_1.pdf: 1197982 bytes, checksum: 344557c29e4105a048177410482f40ca (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / O processo de desenvolvimento de software está sujeito a inserção de erros diversos cuja presença compromete a qualidade final dos produtos de software. Teste é uma atividade dinâmica e bastante custosa dentro das várias empregadas pela Garantia da Qualidade de Software. O objetivo de teste é demonstrar que um comportamento específico (cenário) de um sistema foi bem (passou no teste) ou mal sucedido (falhou no teste), através de um veredicto. Automação de testes visa tornar o processo mais ágil em atividades repetitivas e menos suscetível a erros humanos. Existem várias abordagens de geração automática de teste, baseadas na representação formal do comportamento do sistema, que empregam diferentes critérios de seleção para os testes. Quando o objetivo do teste é focar na investigação de certas propriedades ou comportamentos importantes do sistema a ser testado, podemos utilizar o critério de seleção denominado propósito de teste (test purposes). CSP (Communicating Sequential Processes) é uma notação formal bastante expressiva, uma álgebra de processos útil para especificar comportamentos de sistemas concorrentes e distribuídos, de hardware e software. Infelizmente, não existe na literatura abordagens para geração de testes diretamente a partir de álgebras de processo como CSP. As abordagens existentes utilizam a representação operacional (sistemas de transições rotuladas LTS) dos processos CSP. O objetivo deste trabalho é introduzir uma estratégia para geração automática de testes consistentes (sound), elaborada inteiramente a partir da semântica denotacional de CSP (notação de processos e modelos semânticos). É definida uma teoria de testes baseada na Teoria de Testes de Tretmans. Um ponto comum entre estas teorias é que o conjunto de ações de entrada e saída para especificações (alfabetos), implementações e testes são separados, de forma a definir com precisão os veredictos para execução dos testes e a relação de conformidade entre implementação e especificação. Adicionalmente, uma relação de conformidade denotada cspioco é introduzida em termos de refinamentos de processos para determinar se o processo que representa a implementação a ser testada está coerente com o comportamento do processo da especificação. É apresentada, ainda, a estrutura e a utilização de uma ferramenta implementada com o propósito de avaliar esta abordagem dentro do ambiente de teste de um projeto de pesquisa que envolve uma cooperação entre o CIn-UFPE e a Motorola Industrial Limitada. Alguns experimentos práticos foram realizados neste contexto

O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL. / This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL. / This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

Este trabalho reflete os esforcos realizados no estudo das principais técnicas automaticas de verificacao de sistemas que podem ser modelados em Maquinas de Estados Finitas, em particular as que normalmente se enquadram dentro da denominacao de model checking (verificacao de modelos). De modo a permitir ao leitor uma compreensao das vantagens e desvantagens de cada tecnica, os fundamentos teoricos de cada uma delas sao apresentados e ilustrados atraves de exemplos. Alem de uma apresentacao da teoria associada a cada tecnica, esta dissertação ainda apresenta dois estudos de caso de interesse bastante pratico: a verificacao de propriedades de um sistema de manufatura originalmente modelado atraves de uma rede de Petri e a verificacao de propriedades do intertravamento de uma seção metroviaria. Os dois estudos de caso utilizam tecnicas denominadas simbolicas. No primeiro estudo de caso, propoe-se que as invariantes obtidas da equação de estado sejam acrescentadas ao modelo a ser verificado, o que permite a obtenção de ganhos de desempenho na verificacao. O segundo estudo de caso e resolvido a partir da utilizacao de um procedimento proposto nesta dissertacao. Este procedimento permite a verificacao de algumas propriedades de seguranca sem que a verificacao se inviabilize devido a explosao no numero de estados. A utilizacao deste procedimento permite a verificacao de propriedades de uma secao de intertravamento com cerca de 2000 variaveis digitais em questao de poucos segundos.A principal conclusao a que este trabalho chega e consequencia dos resultados positivos observados nos estudos de caso: o model checking simbólico parece possuir um amplo campo de aplicacoes ainda por ser mais bem explorado / This work is the result of the efforts oriented to the study of the main automatic verification techniques for systems that can be modeled as Finite State Machines, in particular of those techniques which are generally called as model checking. In order to make the reader able to understand the pros and cons of each technique, the theory associated to each one is presented, as well as some examples. This work also presents two case studies of practical interest, both of each were solved with techniques which are called symbolic. The first one is the verification of some properties of a manufacturing system originally modeled by a Petri net. In order to improve the verification performance, it is proposed that the model to be verified be enlarged with the inclusion of the invariants calculated with the help of the state equation. The second case study is the verification of some safety properties of an interlocking system of a subway section. The verification is carried out with the help of a procedure which is proposed in this work. The aim of such a procedure is to bypass the state explosion problem, in order to make the verification feasible. It was possible to verify an interlocking system with about 2000 digital variables in a matter of few seconds. The main conclusion of the work comes from the positive results reached by both case studies: it seems to be a large number of applications yet to be explored in which symbolic model checking may be considered.

Entre as principais dificuldades do desenvolvimento de software embarcado crítico e de tempo real está a especificação e o processo de verificação e validação apoiado ao projeto conceitual. Neste contexto, a modelagem de sistemas tem uma importante função, uma vez que um processo complexo possa ser analisado e validado antes de sua real implementação. Esta dissertação aborda o problema de verificação e validação de software embarcado de um satélite com configuração ACDH (Attitude Control and Data Handling) através de uma plataforma aerosuspensa com um grau de liberdade, utilizando a SysML, a ferramenta CASE TELELOGIC Rhapsody e a orientação das normas da ECSS (European Cooperation on Space Standardization). A partir do modelo obtido, são utilizadas três abordagens para análise e avaliação: (1) Especificação e gerenciamento dos requisitos, através dos conceitos determinados pela ECSS; (2) Modelagem do sistema e verificação dos requisitos, através do formalismo matemático dos autômatos utilizando a técnica de model checking através da ferramenta UPPAL; (3) Conversão do modelo em SysML, aplicando a Engenharia de Requisitos e o processo de verificação e validação do sistema, através da simulação na ferramenta CASE.

Este trabalho reflete os esforcos realizados no estudo das principais técnicas automaticas de verificacao de sistemas que podem ser modelados em Maquinas de Estados Finitas, em particular as que normalmente se enquadram dentro da denominacao de model checking (verificacao de modelos). De modo a permitir ao leitor uma compreensao das vantagens e desvantagens de cada tecnica, os fundamentos teoricos de cada uma delas sao apresentados e ilustrados atraves de exemplos. Alem de uma apresentacao da teoria associada a cada tecnica, esta dissertação ainda apresenta dois estudos de caso de interesse bastante pratico: a verificacao de propriedades de um sistema de manufatura originalmente modelado atraves de uma rede de Petri e a verificacao de propriedades do intertravamento de uma seção metroviaria. Os dois estudos de caso utilizam tecnicas denominadas simbolicas. No primeiro estudo de caso, propoe-se que as invariantes obtidas da equação de estado sejam acrescentadas ao modelo a ser verificado, o que permite a obtenção de ganhos de desempenho na verificacao. O segundo estudo de caso e resolvido a partir da utilizacao de um procedimento proposto nesta dissertacao. Este procedimento permite a verificacao de algumas propriedades de seguranca sem que a verificacao se inviabilize devido a explosao no numero de estados. A utilizacao deste procedimento permite a verificacao de propriedades de uma secao de intertravamento com cerca de 2000 variaveis digitais em questao de poucos segundos.A principal conclusao a que este trabalho chega e consequencia dos resultados positivos observados nos estudos de caso: o model checking simbólico parece possuir um amplo campo de aplicacoes ainda por ser mais bem explorado / This work is the result of the efforts oriented to the study of the main automatic verification techniques for systems that can be modeled as Finite State Machines, in particular of those techniques which are generally called as model checking. In order to make the reader able to understand the pros and cons of each technique, the theory associated to each one is presented, as well as some examples. This work also presents two case studies of practical interest, both of each were solved with techniques which are called symbolic. The first one is the verification of some properties of a manufacturing system originally modeled by a Petri net. In order to improve the verification performance, it is proposed that the model to be verified be enlarged with the inclusion of the invariants calculated with the help of the state equation. The second case study is the verification of some safety properties of an interlocking system of a subway section. The verification is carried out with the help of a procedure which is proposed in this work. The aim of such a procedure is to bypass the state explosion problem, in order to make the verification feasible. It was possible to verify an interlocking system with about 2000 digital variables in a matter of few seconds. The main conclusion of the work comes from the positive results reached by both case studies: it seems to be a large number of applications yet to be explored in which symbolic model checking may be considered.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-23T13:23:08Z No. of bitstreams: 1 DANIEL AGUIAR DA SILVA - DISS PPGCC 2006..pdf: 730843 bytes, checksum: e5d7ebe87ab82d200f68fb0b5b0df784 (MD5) / Made available in DSpace on 2018-08-23T13:23:08Z (GMT). No. of bitstreams: 1 DANIEL AGUIAR DA SILVA - DISS PPGCC 2006..pdf: 730843 bytes, checksum: e5d7ebe87ab82d200f68fb0b5b0df784 (MD5) Previous issue date: 2006-05-26 / Técnicas e ferramentas de testes formais baseados em modelos têm sido desenvolvidas para tornar mais rigoroso e eficiente o processo de teste de sistemas reativos com características de distribuição e concorrência. O não-determinismo inerente a estes sistemas torna os difíceis de serem testados, devido à alta complexidade de obtenção das configurações necessárias para execução dos casos de teste. As propriedades especificadas para estes sistemas são a base para a geração dos casos de teste de conformidade, que devem avaliar a correspondência entre modelo e código. Estas propriedades, denominadas objetivos de teste, devem ser especificadas de maneira a guiar a geração dos casos de teste. Entretanto, a especificação dos objetivos de teste a partir de modelos complexos como os destes sistemas ainda carece de técnicas e ferramentas apropriadas, tornando esta atividade propensa a erros. Os casos de teste podem assim, ter efetividade afetada em caso de erros na especificação dos objetivosdeteste. Comoobjetivodecontribuirparaasoluçãodesteproblema,estetrabalho apresenta técnica de geração de objetivos de teste para sistemas reativos, baseando-se na técnica de verificação de modelos CTL. A técnica proposta visa usufruir da eficiência dos algoritmos da verificação de modelos, por meio de sua adaptação para a análise destes, para a geração dos objetivos de teste. / Techniques and tools for model based testing have been developed to make the process of testing distributed concurrent reactive systems more efficient and rigorous. The inherent nondeterminism of these systems can make it difficult to test them due to the complex process of obtaining test cases configurations from models. To better guide the testing process, properties specified to these systems are used as basis for the test case generation. Such properties, called test purposes, shall be exhibitedby the implementation under test through test case execution. However, specifying test purposes from the common complex and large models of these systems suffers from the lack of appropriated tools and techniques, making it error-prone and inadequate. Thus, test cases based on such test purposes may be affected, getting no desirable soundness. Aiming at solving this problem, we present a technique for test purpose generation for reactive systems based on the CTL model checking technique. We aim at taking benefit from the efficiency of model checking algorithms to better analyze the models to generate the test purposes.

Tendo em vista a crescente demanda da região metropolitana de São Paulo por transporte público rápido e eficaz, os investimentos em novas linhas e estações de metrô são crescentes, bem como a necessidade de aceleração do projeto e construção de tal infraestrutura. Nesse contexto insere-se a implantação do processo BIM - \"Building Information Modeling\" ou \"Modelagem da Informação da Construção\" pela Companhia do Metropolitano de São Paulo em seus projetos de estações e vias. O Metrô atua produzindo projetos internamente e, principalmente, contratando projetos externos que necessitam de análise para aprovação. Com o desenvolvimento dos projetos básicos civis em BIM, houve alterações no trabalho diário, a análise visual se beneficiou do modelo 3D, representando agora o projeto inteiro e não apenas seções deste. Isto possibilitou antecipar decisões que antes eram tomadas no executivo, atuando assim em um momento com maior capacidade de alterações de projeto. Um dos usos importantes do BIM no processo de análise de projeto é a Verificação de Regras. O uso de verificação automatizada permite que o analista possa focar apenas na lista de não conformidades, ganhando tempo para dedicar-se mais a resolução destas. E, por parte do projetista, é possível verificar antecipadamente o cumprimento de diretrizes, e já providenciar soluções aos problemas apontados. A presente pesquisa visou apoiar o processo de implantação deste uso de BIM, pela proposta de fluxo para implantação da verificação automatizada, identificação dos padrões de regras existentes e desenvolvimento de uma classificação de regras com foco na automatização de sua verificação. Os padrões propostos foram usados na análise de documento de Instruções de Projeto Básico de Arquitetura e na tradução de suas regras para aplicação em software para este fim com a intenção de fechar o ciclo da verificação. / In view of the increasing demand of São Paulo metropolitan area for fast and efficient public transport, the investment in new lines and subway stations are growing, as well as the need for accelerating the design and the construction of such infrastructure. In this context is the deployment of BIM - \"Building Information Modeling\" by Companhia do Metropolitano de São Paulo - Metrô on its stations and rails. Metrô operates the production of projects internally, and particularly contracts external projects that require analysis for approval. With the development of their basic civil projects in BIM, there have been changes in daily work, the visual analysis has been benefited from the 3D model, representing now the entire project and not only its sections. This has made possible to anticipate decisions that used to be taken in the shop drawings phase, thereby acting at a time with greater ability to apply changes in projects. One of the important BIM usages in the project\'s review process is the code checking. This allows the analyst to focus on the list of nonconformities only, gaining time to make further effort on their resolution. And, on the part of the designer, it is possible to verify the compliance of the guidelines in advance, and provide solutions to the problems already presented. The present research aimed to support the implementation process of using this BIM use, based on the flow proposal for the deployment of automated verification, the identification of patterns of existing rules and the developing of classification rules focusing on automating its checking. The proposed standards were used when analyzing documents of the architecture basic design instructions and in the translation of their rules for software application for this purpose with the intention to close the checking cycle.