@MastersThesis{RohdeEras:2021:MéGeAu,
author = "Rohde Eras, Eduardo",
title = "Singularity: um m{\'e}todo para gera{\c{c}}{\~a}o
autom{\'a}tica de casos de teste unit{\'a}rios baseado em
contraexemplos de verificador de modelos para
aplica{\c{c}}{\~o}es em C++",
school = "Instituto Nacional de Pesquisas Espaciais (INPE)",
year = "2021",
address = "S{\~a}o Jos{\'e} dos Campos",
month = "2020-05-26",
keywords = "casos de teste de software, teste unit{\'a}rio, verificador de
modelo, automatiza{\c{c}}{\~a}o de teste, aplica{\c{c}}{\~o}es
em C++, software testing cases, unit testing, model checking, test
automation, C++ applications.",
abstract = "Uma das tarefas mais desafiadoras na atividade de teste de
software {\'e} a gera{\c{c}}{\~a}o de casos/dados de teste.
Embora haja uma quantidade significativa de estudos nesse sentido,
ainda {\'e} necess{\'a}rio avan{\c{c}}ar em dire{\c{c}}{\~a}o
a abordagens que possam gerar casos/dados de teste com base apenas
no c{\'o}digo-fonte, considerando que muitos sistemas possuem
apenas o c{\'o}digo-fonte, sem a exist{\^e}ncia de uma
documenta{\c{c}}{\~a}o adequada. Esta Disserta{\c{c}}{\~a}o de
Mestrado apresenta um novo m{\'e}todo, denominado Singularity,
para a gera{\c{c}}{\~a}o de casos de teste unit{\'a}rios a
partir de c{\'o}digo-fonte em C++ e utilizando
verifica{\c{c}}{\~a}o de modelos, sendo este um m{\'e}todo de
Verifica{\c{c}}{\~a}o Formal. Na presente abordagem, que {\'e}
apoiada por uma ferramenta, o c{\'o}digo-fonte C++ {\'e}
traduzido automaticamente para modelos intermedi{\'a}rios
(M{\'a}quina de Estados Finitos, Grafo de Fluxo de Controle) e
depois para a nota{\c{c}}{\~a}o do Verificador de Modelos NuSMV.
Posteriormente, uma t{\'e}cnica baseada no m{\'e}todo HiMoST e
em propriedades reconhecidas na literatura como {"}armadilha{"}
produzem contraexemplos do verificador de modelos que s{\~a}o, de
fato, os casos de teste abstratos em si. O m{\'e}todo Singularity
foi aplicado a um conjunto de c{\'o}digos em C++
extra{\'{\i}}do de duas ferramentas complexas de sensoriamento
remoto desenvolvidas no Instituto Nacional de Pesquisas Espaciais
(INPE). Os resultados demonstraram a viabilidade do m{\'e}todo
para a gera{\c{c}}{\~a}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.",
committee = "Andrade Neto, Pedro Ribeiro de (presidente) and Santiago
J{\'u}nior, Valdivino Alexandre de (orientador) and
Mattiello-Francisco, Maria de F{\'a}tima and Ferrari, Fabiano
Cutigi",
englishtitle = "Singularity: a method for automatic generation of unit test cases
based on model checker counterexamples of C++ applications",
language = "pt",
pages = "97",
ibi = "8JMKD3MGP3W34R/42L2BFE",
url = "http://urlib.net/ibi/8JMKD3MGP3W34R/42L2BFE",
targetfile = "publicacao_FA provisoria.pdf",
urlaccessdate = "29 mar. 2024"
}