Geração de casos de teste usando Bounded Model Checking

Menezes, Rafael Sá; http://lattes.cnpq.br/9276676299919657; https://orcid.org/0000-0002-6102-4343

Dissertação

Geração de casos de teste usando Bounded Model Checking

A geração automática de casos de teste consiste na geração de entradas para um algoritmo que sejam capazes de explorar todos os caminhos de um programa, maximizando a cobertura. Comumente, técnicas como fuzzing são utilizadas para isso por sua performance alta e de custo baixo. Entretanto, técnicas...

ver descrição completa

Autor principal:	Menezes, Rafael Sá
Outros Autores:	http://lattes.cnpq.br/9276676299919657, https://orcid.org/0000-0002-6102-4343
Grau:	Dissertação
Idioma:	por
Publicado em:	Universidade Federal do Amazonas 2021
Assuntos:	Fuzzing Sistema de transição Agoritmo de slicing Operações bit a bit Sistema de armazenamento CIÊNCIAS EXATAS E DA TERRA Bounded model checking Caching Software Verification SMT solving Testcase generation
Acesso em linha:	https://tede.ufam.edu.br/handle/tede/8447

id	oai:https:--tede.ufam.edu.br-handle-:tede-8447
recordtype	dspace
spelling	oai:https:--tede.ufam.edu.br-handle-:tede-84472021-09-17T05:03:28Z Geração de casos de teste usando Bounded Model Checking Menezes, Rafael Sá Cordeiro, Lucas Carvalho http://lattes.cnpq.br/9276676299919657 http://lattes.cnpq.br/5005832876603012 Barreto, Raimundo da Silva http://lattes.cnpq.br/1132672107627968 Lima Filho, Eddie Batista de http://lattes.cnpq.br/7827981023232761 https://orcid.org/0000-0002-6102-4343 Fuzzing Sistema de transição Agoritmo de slicing Operações bit a bit Sistema de armazenamento CIÊNCIAS EXATAS E DA TERRA Bounded model checking Caching Software Verification SMT solving Testcase generation A geração automática de casos de teste consiste na geração de entradas para um algoritmo que sejam capazes de explorar todos os caminhos de um programa, maximizando a cobertura. Comumente, técnicas como fuzzing são utilizadas para isso por sua performance alta e de custo baixo. Entretanto, técnicas formais, como execução simbólica, vêm ganhando espaço nesse domínio, entre elas, a Bounded Model Checking (BMC). BMC é uma técnica de verificação que codifica uma propriedade em caminhos de um sistema de transição até um limite k, resultando em uma única fórmula lógica que, caso contenha uma violação, irá gerar uma prova. Essa prova - embora reduzida - contém informações que podem ser utilizadas como base para a geração de um caso de teste. A dificuldade de usar BMC em casos de teste está na complexidade de tempo/espaço da técnica e nas simplificações feitas para tentar contornar isso (simplificações, estratégias). Incremental BMC é uma estratégia que, de forma incremental, aumenta esse limite k até que uma violação seja encontrada ou que o sistema seja completamente verificado. Entretanto, cada caminho do sistema é reverificado a cada incremento, o que adiciona tempo e consumo de memória para resolver a instância atual. Para resolver esses problemas, este trabalho propõe duas contribuições: (1) algoritmo de geração de casos de teste a partir de provas e (2) um sistema de cache que utiliza soluções de instâncias menores através de (A) uso direto das instâncias anteriores; e (B) uso indireto através de fórmulas de outros sistemas. Essas contribuições foram implementadas no Efficient SMT-based Bounded Model Checker (ESBMC), sendo testadas em situações de Integração Contínua (CI) e sobre benchmarks públicos de programas em C, obtendo a primeira colocação na competição TestComp’21 na categoria reach-error e reduzindo o tempo do CI. Testcase generation consists in generating inputs for an algorithm that are able to explore all paths of a program, maximizing its coverage. Usually, fuzzing techniques are used because of its great performace and low cost. However, formal techniques such as Symbolic Execution are gaining notority in this domain, one of those is Bounded Model Checking (BMC). BMC is a verification technique that encodes a property in paths of transition system up to a bound k to one single logic formula such that if the system contains a flaw the formula will generate a proof. This proof contain information for the testcase generation. The difficult of using BMC for testcase is at the time/space complexity and at the optimizations trying to workaround this issue. Incremental BMC is a strategy that increases the k limit until the violation is found or the system is completely verified. The issue is that at each increment every path is verified again, which add time and memory consuption to solve the current instance. To solve those issue this work proposes two main contributions: (1) algorithm for testcase generation using proofs; and (2) a caching system that uses small instances by: (A) direct use; and (B) indirect use of other systems. Those contributions were implemented into the Efficient SMT-based Bounded Model Checker (ESBMC), being tested over Continuos Integration and over public benchmarks of C programs, obtaining the first place at TestComp’21 in the Cover-error category and reducing the time of the CI. CNPq - Conselho Nacional de Desenvolvimento Científico e Tecnológico 2021-09-16T15:03:38Z 2021-06-08 Dissertação MENEZES, Rafael Sá. Geração de casos de teste usando Bounded Model Checking. 2021. 54 f. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas, Manaus, 2021. https://tede.ufam.edu.br/handle/tede/8447 por Acesso Aberto http://creativecommons.org/licenses/by/4.0/ application/pdf Universidade Federal do Amazonas Instituto de Computação Brasil UFAM Programa de Pós-graduação em Informática
institution	TEDE - Universidade Federal do Amazonas
collection	TEDE-UFAM
language	por
topic	Fuzzing Sistema de transição Agoritmo de slicing Operações bit a bit Sistema de armazenamento CIÊNCIAS EXATAS E DA TERRA Bounded model checking Caching Software Verification SMT solving Testcase generation
spellingShingle	Fuzzing Sistema de transição Agoritmo de slicing Operações bit a bit Sistema de armazenamento CIÊNCIAS EXATAS E DA TERRA Bounded model checking Caching Software Verification SMT solving Testcase generation Menezes, Rafael Sá Geração de casos de teste usando Bounded Model Checking
topic_facet	Fuzzing Sistema de transição Agoritmo de slicing Operações bit a bit Sistema de armazenamento CIÊNCIAS EXATAS E DA TERRA Bounded model checking Caching Software Verification SMT solving Testcase generation
description	A geração automática de casos de teste consiste na geração de entradas para um algoritmo que sejam capazes de explorar todos os caminhos de um programa, maximizando a cobertura. Comumente, técnicas como fuzzing são utilizadas para isso por sua performance alta e de custo baixo. Entretanto, técnicas formais, como execução simbólica, vêm ganhando espaço nesse domínio, entre elas, a Bounded Model Checking (BMC). BMC é uma técnica de verificação que codifica uma propriedade em caminhos de um sistema de transição até um limite k, resultando em uma única fórmula lógica que, caso contenha uma violação, irá gerar uma prova. Essa prova - embora reduzida - contém informações que podem ser utilizadas como base para a geração de um caso de teste. A dificuldade de usar BMC em casos de teste está na complexidade de tempo/espaço da técnica e nas simplificações feitas para tentar contornar isso (simplificações, estratégias). Incremental BMC é uma estratégia que, de forma incremental, aumenta esse limite k até que uma violação seja encontrada ou que o sistema seja completamente verificado. Entretanto, cada caminho do sistema é reverificado a cada incremento, o que adiciona tempo e consumo de memória para resolver a instância atual. Para resolver esses problemas, este trabalho propõe duas contribuições: (1) algoritmo de geração de casos de teste a partir de provas e (2) um sistema de cache que utiliza soluções de instâncias menores através de (A) uso direto das instâncias anteriores; e (B) uso indireto através de fórmulas de outros sistemas. Essas contribuições foram implementadas no Efficient SMT-based Bounded Model Checker (ESBMC), sendo testadas em situações de Integração Contínua (CI) e sobre benchmarks públicos de programas em C, obtendo a primeira colocação na competição TestComp’21 na categoria reach-error e reduzindo o tempo do CI.
author_additional	Cordeiro, Lucas Carvalho
author_additionalStr	Cordeiro, Lucas Carvalho
format	Dissertação
author	Menezes, Rafael Sá
author2	http://lattes.cnpq.br/9276676299919657 https://orcid.org/0000-0002-6102-4343
author2Str	http://lattes.cnpq.br/9276676299919657 https://orcid.org/0000-0002-6102-4343
title	Geração de casos de teste usando Bounded Model Checking
title_short	Geração de casos de teste usando Bounded Model Checking
title_full	Geração de casos de teste usando Bounded Model Checking
title_fullStr	Geração de casos de teste usando Bounded Model Checking
title_full_unstemmed	Geração de casos de teste usando Bounded Model Checking
title_sort	geração de casos de teste usando bounded model checking
publisher	Universidade Federal do Amazonas
publishDate	2021
url	https://tede.ufam.edu.br/handle/tede/8447
_version_	1831969986035318784
score	11.753896

Geração de casos de teste usando Bounded Model Checking

Registros relacionados