Dissertação

JMLCUTE: Automated JML-Based Unit Test Case Generation EVALUATED

Uma especificação formal é uma descrição detalhada do comportamento de um método. Especificações formais podem auxiliar o desenvolvimento de software servindo de documentação para métodos complexos. Algumas ferramentas de verificação de software suportam especificações formais para detetar errors num programa e gerar automaticamente uma mensagem de erro ou um caso de teste representativo. No entanto, ferramentas de verificação existentes que detetam erros automaticamente e suportam especificações formais não conseguem extrair informação de métodos complexos ou cuja implementação é desconhecida, e terminam com uma verificação incompleta. Esta dissertação propõe JMLCUTE: a primeira ferramenta que deteta errors num programa automaticamente, suporta especificações formais e usa verificação ``concólica'' - uma técnica que analisa a execução do programa para lidar com métodos complexos ou desconhecidos. Esta dissertação também apresenta uma avaliação que testa o quanto especificações formais e a verificação ``concólica'' se auxiliam para gerar casos de teste novos e interessantes. A avaliação compara JMLCUTE com uma ferramenta de verificação ``concólica'' que não suporta especificações formais, jCUTE. Os resultados da avaliação mostram que JMLCUTE encontra erros de especificação que jCUTE ignora, e que os tempos de execução de ambas as ferramentas é semelhante para projectos complexos.
geração automática de casos de teste, desenvolvimento orientado a teste, verificação de programas, especificação formal, execução simbólica, execução concólica

Novembro 3, 2015, 9:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

João Carlos Serrenho Dias Pereira

Departamento de Engenharia Informática (DEI)

Professor Auxiliar

ORIENTADOR

Pedro Miguel dos Santos Alves Madeira Adão

Departamento de Engenharia Informática (DEI)

Professor Auxiliar