Geração de entrada de teste com Java PathFinder

Mostramos como a verificação de modelos e a execução simbólica podem ser usadas para gerar entradas de teste para alcançar a cobertura estrutural de código que manipula estruturas de dados complexas. Focamos em obter cobertura de ramificação durante os testes unitários de alguns dos métodos principais da implementação da árvore rubro-negra na biblioteca Java TreeMap, utilizando o verificador de modelos Java PathFinder. Três técnicas diferentes de geração de testes serão introduzidas e comparadas, a saber, a verificação direta de modelos do código, a verificação de modelos usada de forma de caixa-preta para gerar todas as entradas até um tamanho fixo e, por último, a verificação de modelos usada durante a geração de entrada de teste de caixa-branca. A principal contribuição deste trabalho é mostrar como a geração eficiente de entrada de teste de caixa-branca pode ser feita para código que manipula dados complexos, levando em conta pré-condições de métodos complexas.