Um estudo empírico sobre geração de testes com BETA: Avaliação e aperfeiçoamento

Abstract

The demand for secure and robust systems has made to grow the concern for developing quality software. Software Testing and Formal Methods are two approaches that have this purpose. In this context, several efforts are being made to unite these two approaches, which can complement each other and bring more quality to the software. In one of these efforts, the approach and tool BETA (B Based Testing Approach) was developed. BETA generates unit tests from formal specifications written in B Method notation. The present work aims to contribute with the evolution and improvement of the approach and tool BETA. For this purpose, two lines of action were taken. In the first line of action, this work brought contributions for the last two stages of the BETA approach. For the penultimate stage, the test oracles definition, this work proposed test oracles strategies that brought more flexibility and a better definition for the stage. For the last stage, the concrete tests implementation, this work developed a test scripts generator that automates part of the implementation and, thus, contribute to reduce the effort spent in the stage. In the second line of action, this work performed an empirical study to evaluate the approach and tool. Thus, BETA was applied in two case studies that had different objectives and complexities. In the first case study, BETA was used to generate tests for the API of the Lua programming language. In the second case study, BETA was used to contribute to the validation of two code generators for the B Method, the b2llvm and C4B. In both case studies, the results of BETA were evaluated quantitatively and qualitatively. With this study, this work was able to identify qualities and limitations of BETA and, with that, establish a basis for proposing improvements to the approach and tool.