{pt_PT=JMLCUTE: Automated JML-Based Unit Test Case Generation} {} EVALUATED

Detalhes: {pt=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., en=A formal specification is the detailed description of a function's behaviours. Formal specification can be helpful during development by providing a formal documentation on the behaviour of complex functions. Some verification tools already support formal specifications to automatically detect program errors and automatically generate a useful error message or a representative test case. However, existing verification tools that automatically detect program errors and support formal specifications cannot extract information from unknown or complex functions and end up with an incomplete verification. This dissertation proposes JMLCUTE: the first tool to automatically detect program errors, support a formal specification and use concolic testing - a method that uses both program and run-time analysis to deal with unknown or complex functions. This dissertation also presents an evaluation on how formal specification and concolic testing use each other to generate new and interesting test cases. The evaluation compares JMLCUTE with a similar concolic testing tool that does not support formal specifications, jCUTE. Evaluation results show that JMLCUTE can find specification errors that jCUTE ignores, and that both tools' execution times are similar for complex projects.}

Discussão: novembro 3, 2015, 9:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

AUTOR

Rafael Farias Baltazar (ist170116)

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