Tópicos Avançados em
Engenharia de Software
Generating Tests from Counterexamples
Allynson Praxedes
Leonardo Nunes
Resumo
Software model Checker extendido do BLAST
-Conjunto de Vetores de testes
-Localizações do programa
(Predicado P verdadeiro)
Código morto
Model Checker
Execução do programa viola uma especificação
do mesmo.
Caminho falhos ou Caminhos que violam a
especificação
Executa até encontrar um Counterexample
Overview
Fase 1: Model checking
• Encontrar o vetor teste que leva o programa
para a localização L5;
• m=z; assume (y<z); assume (x<y);
• Os passos para a execução do programa
alcançar L5 no CFA  Counterexemple
Fase 2: Tests from counterexamples
• Encontrar um vetor teste – valores associados
a x, y e z – que alcance L5;
• trace formula (TF) – conjunção das restrições:
– (m = z) ^ (y < z) ^ (x < y)
– “x=0,y=1,z=2,m=2”
Continuação
• Repetir as duas fases até para cada localização
• Até produzir um conjunto de vetores teste
para todas as localizações de CFA.
• Localizações não são alcansáveis: L13 e L15
Executando testes
• Construir o Test Driver para o programa dado;
• Utilizando o BLAST’s testdriver generator;
• Aceita como entrada os vetores de teste
gerados;
• Executa os testes.