| Summary: | Made available in DSpace on 2014-12-17T15:47:51Z (GMT). No. of bitstreams: 1
FernandaMS_DISSERT_cad.pdf: 1351543 bytes, checksum: 27a89b596f5bafb661e158d68cfc729c (MD5)
Previous issue date: 2010-03-29 === 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
|
|---|
