%0 Thesis
%4 sid.inpe.br/mtc-m21c/2020/06.08.20.44
%2 sid.inpe.br/mtc-m21c/2020/06.08.20.44.11
%T Singularity: um método para geração automática de casos de teste unitários baseado em contraexemplos de verificador de modelos para aplicações em C++
%J Singularity: a method for automatic generation of unit test cases based on model checker counterexamples of C++ applications
%D 2021
%8 2020-05-26
%9 Dissertação (Mestrado em Computação Aplicada)
%P 97
%A Rohde Eras, Eduardo,
%E Andrade Neto, Pedro Ribeiro de (presidente),
%E Santiago Júnior, Valdivino Alexandre de (orientador),
%E Mattiello-Francisco, Maria de Fátima,
%E Ferrari, Fabiano Cutigi,
%I Instituto Nacional de Pesquisas Espaciais (INPE)
%C São José dos Campos
%K casos de teste de software, teste unitário, verificador de modelo, automatização de teste, aplicações em C++, software testing cases, unit testing, model checking, test automation, C++ applications.
%X Uma das tarefas mais desafiadoras na atividade de teste de software é a geração de casos/dados de teste. Embora haja uma quantidade significativa de estudos nesse sentido, ainda é necessário avançar em direção a abordagens que possam gerar casos/dados de teste com base apenas no código-fonte, considerando que muitos sistemas possuem apenas o código-fonte, sem a existência de uma documentação adequada. Esta Dissertação de Mestrado apresenta um novo método, denominado Singularity, para a geração de casos de teste unitários a partir de código-fonte em C++ e utilizando verificação de modelos, sendo este um método de Verificação Formal. Na presente abordagem, que é apoiada por uma ferramenta, o código-fonte C++ é traduzido automaticamente para modelos intermediários (Máquina de Estados Finitos, Grafo de Fluxo de Controle) e depois para a notação do Verificador de Modelos NuSMV. Posteriormente, uma técnica baseada no método HiMoST e em propriedades reconhecidas na literatura como "armadilha" produzem contraexemplos do verificador de modelos que são, de fato, os casos de teste abstratos em si. O método Singularity foi aplicado a um conjunto de códigos em C++ extraído de duas ferramentas complexas de sensoriamento remoto desenvolvidas no Instituto Nacional de Pesquisas Espaciais (INPE). Os resultados demonstraram a viabilidade do método para a geração de casos de teste. ABSTRACT: One of the most challenging tasks in software testing activity is the generation of test cases/data. Although there is a significant amount of studies in this direction, it is still necessary to move towards approaches that can generate test cases/data based only on the source code, since many systems have only the source code, without necessarily the existence of adequate documentation. This Master Dissertation presents a new method, called Singularity, for the generation of unit test cases/data from C++ source codes using Model Checking, a Formal Verification method. In the present approach, which is supported by a tool, the C++ source code is automatically translated into intermediate models (Finite State Machine, Control Flow Graph) and then into the NuSMV model checker notation. Subsequently, a technique based on the HiMoST method and the called "trap properties" produces counterexamples of the model checker which are, in fact, the test cases/data itself. The Singularity method was applied to a set of C++ codes extracted from two complex remote sensing tools developed at the National Institute for Space Research (INPE). The results demonstrated the viability of the method for generating test cases/data.
%@language pt
%3 publicacao_FA provisoria.pdf