Ferramenta para Geração Automática de Testes Unitários a patir de Especificações Algébricas usando Alloy e SMT

• Main Author: Tiago Faria Campos
• Other Authors: Faculdade de Engenharia
• Format: Others
• Language: Portuguese
• Published: 2019
• Subjects: Ciências da engenharia e tecnologias; Engineering and technology
• Online Access: https://repositorio-aberto.up.pt/handle/10216/76359

No âmbito do projeto QUEST (http://gloss.di.fc.ul.pt/quest), a equipa da FEUP desenvolveu uma ferramenta (GenT) de geração automática de testes unitários em JUnit a partir de especificações formais de tipos abstratos de dados, envolvendo os seguintes passos: tradução da especificação formal para Alloy; geração automática de objetivos de teste (condições a testar); utilização do Alloy Analyzer para encontrar modelos que satisfazem os objetivos de teste; conversão automática dos modelos encontrados para testes em JUnit e "mock objects" associados. A ferramenta desenvolvida precisa de ser continuada para melhorar a adequação dos testes gerados, nomeadamente: alguns dos objetivos de teste gerados (condições a testar) não são satisfazíveis; não gera testes fora do domínio (teste de excepções). O objetivo do presente trabalho é precisamente resolver as limitações atuais, bem como efetuar uma avaliação experimental que demonstre as vantagens em relação a outras abordagens existentes. Espera-se que a nova versão da ferramenta possa ser utilizada a nível académico no ensino de algoritmos e estruturas de dados e a nível industrial para melhorar o teste de implementações de tipos abstratos de dados. === Under the QUEST (http://gloss.di.fc.ul.pt/quest) project, FEUP team developed a tool(Gent) of automatic generation of unit tests in JUnit from formal specifications of abstract data types, involving the following steps: translation of the formal specification for Alloy; automatic generation of test objectives (test conditions); use the Alloy Analyzer to find models which meet the test objectives; automatic conversion of the models found for JUnit tests and associated "mock objects".The tool developed needs to be continued to improve the adequacy of the generated tests, namely: some of the goals generated test (test conditions) are not satisfiable; does not generate tests outside the field test (exceptions).The objective of this work is precisely to solve the current limitations, as well as place an experimental evaluation to demonstrate the advantages over other existing approaches. It is expected that the new version of the tool can be used in academic teaching of algorithms and data structures and industrial level to improve the implementations of abstract data types test.