Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-02T21:58:30Z No. of bitstreams: 1 WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-09T12:29:25Z (GMT) No. of bitstreams: 1 WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5) / Made available in DSpace on 2018-07-09T12:29:25Z (GMT). No. of bitstreams: 1 WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5) Previous issue date: 2018-05-28 / A lógica linear (LL) tem se consolidado como um bom arcabouço para especificar sistemas computacionais, uma vez que fórmulas podem ser interpretadas como recursos que podem ser consumidos e/ou produzidos. Além disso, do ponto de vista da Teoria da Prova, a LL reconcilia o aspecto construtivo da lógica intuicionista com a simetria da lógica clássica. Desta maneira, é possível, de uma forma mais flexível, modelar estados de um sistema como fórmulas lógicas, e as transições entre esses estados como etapas na construção de uma prova. No entanto, a busca por provas, em geral, não é determinística, pois existem diferentes maneiras de se provar a mesma proposição. Visando reduzir esse problema, um sistema de provas focado pode ser utilizado nesse processo de busca. A grosso modo, um sistema focado considera provas em forma normal, reduzindo assim as ocorrências de provas não essenciais que são sintaticamente diferentes, mas equivalentes no final do processo. Neste trabalho, é apresentada a prova da completude de um sistema focado para a LL, bem como outras propriedades essenciais desse sistema. Além disso, o sistema focado será utilizado para especificar e verificar protocolos de votação, que definem como deve ser escolhido um candidato, feita uma contagem de votos, e divulgado o resultado de uma eleição. Para que isso seja possível, dois protocolos de votação serão especificados formalmente utilizando sistemas de transição de estados, que modelam de forma natural os estados e comportamento de tais protocolos. Junto a isso, para cada sistema, uma especificação em LL será definida e demonstrada que é correta, ou seja, que um passo focado representa uma determinada transição no sistema de estados modelado. Por fim, propriedades inerentes aos protocolos de votação, como a garantia de que o resultado da eleição reflete o desejo dos eleitores, serão apresentadas e demonstradas através de derivações no sistema focado. / Linear logic (LL) has been consolidated as a good framework for specifying computational systems, since formulas can be interpreted as resources that can be consumed and / or produced during a proof. From the point of view of Proof Theory, LL reconciles the constructive aspect of intuitionistic logic with the symmetry of rules in classical logic. Hence, LL offers a more flexible way to model states of a system as well as transitions among those states. We note that the proof search procedure is inherently non-deterministic since there are different ways of proving the same proposition. In order to tame this problem, focused systems have been proposed aiming at reducing the number of choices during the proof search procedure. Roughly, a focused system considers normal form proofs, thus eliminating the occurrences of nonessential proofs that are syntactically different but equivalent. In this work, we present the proof of the completeness of a focused system for LL as well as some other essential properties of this system. In addition, we use the focused system for specifying and verifying voting protocols. Such systems define how a candidate is chosen by tallying votes and computing the final result of an election. We formally specify two voting protocols using transition systems, which naturally model the states and behavior of such protocols. For each system, an encoding in LL is defined and we show that our specification is correct: a focused step corresponds exactly to a transition in the modeled system. Finally, we verify important properties of the voting protocols such as the fact that the system ensures that the election result reflects the voters’ desire.

O Teste Baseado em Modelos (TBM) emergiu como uma estratégia promissora para minimizar problemas relacionados à falta de tempo e recursos em teste de software e visa verificar se a implementação sob teste está em conformidade com sua especificação. Casos de teste são gerados automaticamente a partir de modelos comportamentais produzidos durante o ciclo de desenvolvimento de software. Entre as técnicas de modelagem existentes, Sistemas de Transição com Entrada/Saída (do inglês, Input/Output Transition Systems - IOTSs), são modelos amplamente utilizados no TBM por serem mais expressivos do que Máquinas de Estado Finito (MEFs). Apesar dos métodos existentes para geração de testes a partir de IOTSs, o problema da seleção de casos de testes é um tópico difícil e importante. Os métodos existentes para IOTS são não-determinísticos, ao contrário da teoria existente para MEFs, que fornece garantia de cobertura completa com base em um modelo de defeitos. Esta tese investiga a aplicação de modelos de defeitos em métodos determinísticos de geração de testes a partir de IOTSs. Foi proposto um método para geração de conjuntos de teste com base no método W para MEFs. O método gera conjuntos de teste de forma determinística além de satisfazer condições de suficiência de cobertura da especificação e de todos os defeitos do domínio de defeitos definido. Estudos empíricos avaliaram a aplicabilidade e eficácia do método proposto: resultados experimentais para analisar o custo de geração de conjuntos de teste utilizando IOTSs gerados aleatoriamente e um estudo de caso com especificações da indústria mostram a efetividade dos conjuntos gerados em relação ao método tradicional de Tretmans. / Model-Based Testing (MBT) has emerged as a promising strategy for the minimization of problems related to time and resource limitations in software testing and aims at checking whether the implementation under test is in compliance with its specification. Test cases are automatically generated from behavioral models produced during the software development life cycle. Among the existing modeling techniques, Input/Output Transition Systems (IOTSs) have been widely used in MBT because they are more expressive than Finite State Machines (FSMs). Despite the existence of test generation methods for IOTSs, the problem of selection of test cases is an important and difficult topic. The current methods for IOTSs are non-deterministic, in contrast to the existing theory for FSMs that provides complete fault coverage guarantee based on a fault model. This manuscript addresses the application of fault models to deterministic test generation methods from IOTSs. A method for the test suite generation based on W method for FSMs is proposed for IOTSs. It generates test suites in a deterministic way and also satisfies sufficient conditions of specification coverage and all faults in a given fault domain. Empirical studies evaluated its applicability and effectiveness. Experimental results for the analyses of the cost of test suite generation by random IOTSs and a case study with specifications from the industry show the effectiveness of the test suites generated in relation to the traditional method of Tretmans.

O Teste Baseado em Modelos (TBM) emergiu como uma estratégia promissora para minimizar problemas relacionados à falta de tempo e recursos em teste de software e visa verificar se a implementação sob teste está em conformidade com sua especificação. Casos de teste são gerados automaticamente a partir de modelos comportamentais produzidos durante o ciclo de desenvolvimento de software. Entre as técnicas de modelagem existentes, Sistemas de Transição com Entrada/Saída (do inglês, Input/Output Transition Systems - IOTSs), são modelos amplamente utilizados no TBM por serem mais expressivos do que Máquinas de Estado Finito (MEFs). Apesar dos métodos existentes para geração de testes a partir de IOTSs, o problema da seleção de casos de testes é um tópico difícil e importante. Os métodos existentes para IOTS são não-determinísticos, ao contrário da teoria existente para MEFs, que fornece garantia de cobertura completa com base em um modelo de defeitos. Esta tese investiga a aplicação de modelos de defeitos em métodos determinísticos de geração de testes a partir de IOTSs. Foi proposto um método para geração de conjuntos de teste com base no método W para MEFs. O método gera conjuntos de teste de forma determinística além de satisfazer condições de suficiência de cobertura da especificação e de todos os defeitos do domínio de defeitos definido. Estudos empíricos avaliaram a aplicabilidade e eficácia do método proposto: resultados experimentais para analisar o custo de geração de conjuntos de teste utilizando IOTSs gerados aleatoriamente e um estudo de caso com especificações da indústria mostram a efetividade dos conjuntos gerados em relação ao método tradicional de Tretmans. / Model-Based Testing (MBT) has emerged as a promising strategy for the minimization of problems related to time and resource limitations in software testing and aims at checking whether the implementation under test is in compliance with its specification. Test cases are automatically generated from behavioral models produced during the software development life cycle. Among the existing modeling techniques, Input/Output Transition Systems (IOTSs) have been widely used in MBT because they are more expressive than Finite State Machines (FSMs). Despite the existence of test generation methods for IOTSs, the problem of selection of test cases is an important and difficult topic. The current methods for IOTSs are non-deterministic, in contrast to the existing theory for FSMs that provides complete fault coverage guarantee based on a fault model. This manuscript addresses the application of fault models to deterministic test generation methods from IOTSs. A method for the test suite generation based on W method for FSMs is proposed for IOTSs. It generates test suites in a deterministic way and also satisfies sufficient conditions of specification coverage and all faults in a given fault domain. Empirical studies evaluated its applicability and effectiveness. Experimental results for the analyses of the cost of test suite generation by random IOTSs and a case study with specifications from the industry show the effectiveness of the test suites generated in relation to the traditional method of Tretmans.