Geração de casos de teste a partir de especificações B

With the increasing complexity of software systems, there is also an increased concern about its faults. These faults can cause financial losses and even loss of life. Therefore, we propose in this paper the minimization of faults in software by using formally specified tests. The combination of testing and formal specifications is gaining strength in searches mainly through the MBT (Model-Based Testing). The development of software from formal specifications, when the whole process of refinement is done rigorously, ensures that what is specified in the application will be implemented. Thus, the implementation generated from these specifications would accurately depict what was specified. But not always the specification is refined to the level of implementation and code generation, and in these cases the tests generated from the specification tend to find fault. Additionally, the generation of so-called "invalid tests", ie tests that exercise the application scenarios that were not addressed in the specification, complements more significantly the formal development process. Therefore, this paper proposes a method for generating tests from B formal specifications. This method was structured in pseudo-code. The method is based on the systematization of the techniques of black box testing of boundary value analysis, equivalence partitioning, as well as the technique of orthogonal pairs. The method was applied to a B specification and B test machines that generate test cases independent of implementation language were generated. Aiming to validate the method, test cases were transformed manually in JUnit test cases and the application, created from the B specification and developed in Java, was tested. Faults were found with the execution of the JUnit test cases

Com o crescente aumento da complexidade dos sistemas de software, há também um aumento na preocupação com suas falhas. Essas falhas podem causar prejuízos financeiros e até prejuízos de vida. Sendo assim, propomos neste trabalho a minimização de falhas através de testes em softwares especificados formalmente. A conjunção de testes e especificações formais vem ganhando força na academia principalmente através dos TBM (Testes Baseados em Modelos). O desenvolvimento de software a partir de especificações formais, quando todo o processo de refinamento é feito rigorosamente, garante que o que está especificado será implementado na aplicação. Sendo assim, a implementação gerada a partir destas especificações iria retratar fielmente o que estaria especificado. Mas nem sempre a especificação é refinada até o nível de implementação e geração de código, e nesses casos os testes gerados a partir da especificação tendem a encontrar falhas. Adicionalmente, a geração dos chamados testes inválidos , ou seja, testes que exercitem cenários da aplicação que não foram tratados na especificação, complementa mais significativamente o processo de desenvolvimento formal. Sendo assim, neste trabalho é proposto um método para geração de testes a partir de especificações formais B. Este método foi estruturado em pseudo-código. O método se baseia na sistematização das técnicas de testes caixa preta da análise do valor limite, particionamento de equivalência, bem como da técnica dos pares ortogonais. O método foi aplicado em uma especificação B e foram geradas máquinas B de teste que geram casos de teste independentes de linguagem de implementação. Com o intuito de validação do método, os casos de teste foram transformados manualmente em casos de teste do JUnit e a aplicação, criada a partir da especificação B, e desenvolvida em Java foi testada. Foram encontradas falhas com a execução dos casos de teste JUnit