Beta: uma ferramenta para geração de testes de unidade a partir de especificações B

Formal methods and software testing are tools to obtain and control software quality. When used together, they provide mechanisms for software specification, verification and error detection. Even though formal methods allow software to be mathematically verified, they are not enough to assure that a system is free of faults, thus, software testing techniques are necessary to complement the process of verification and validation of a system. Model Based Testing techniques allow tests to be generated from other software artifacts such as specifications and abstract models. Using formal specifications as basis for test creation, we can generate better quality tests, because these specifications are usually precise and free of ambiguity. Fernanda Souza (2009) proposed a method to define test cases from B Method specifications. This method used information from the machine s invariant and the operation s precondition to define positive and negative test cases for an operation, using equivalent class partitioning and boundary value analysis based techniques. However, the method proposed in 2009 was not automated and had conceptual deficiencies like, for instance, it did not fit in a well defined coverage criteria classification. We started our work with a case study that applied the method in an example of B specification from the industry. Based in this case study we ve obtained subsidies to improve it. In our work we evolved the proposed method, rewriting it and adding characteristics to make it compatible with a test classification used by the community. We also improved the method to support specifications structured in different components, to use information from the operation s behavior on the test case generation process and to use new coverage criterias. Besides, we have implemented a tool to automate the method and we have submitted it to more complex case studies

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior

Métodos formais e testes são ferramentas para obtenção e controle de qualidade de software. Quando utilizadas em conjunto, elas provêem mecanismos para especificação, verificação e detecção de falhas de um software. Apesar de permitir que sistemas sejam matematicamente verificados, métodos formais não são suficientes pra garantir que um sistema esteja livre de defeitos, logo, técnicas de teste de software são necessárias para completar o processo de verificação e validação de um sistema. Técnicas de Testes Baseados em Modelos permitem que testes sejam gerados a partir de outros artefatos de software como especificações e modelos abstratos. Ao utilizarmos especificações formais como base para a criação de testes, podemos gerar testes de melhor qualidade pois estas especificações costumam ser precisas e livres de ambiguidade. Fernanda Souza (2009) propôs um método para definir casos de teste a partir de especificações do Método B. Este método utilizava informações do invariante de uma máquina e das pré-condições de uma operação para definir casos de teste positivos e negativos para tal operação, através de técnicas baseadas em particionamento em classes de equivalência e análise de valor limite. No entanto, a proposta de 2009 não incluía automação e possuía algumas deficiências conceituais como, por exemplo, não se encaixar exatamente em uma classificação de critérios de cobertura bem definida. Iniciamos nosso trabalho com um estudo de caso que aplicou o método a um exemplo de especificação B proveniente da indústria. A partir deste estudo obtivemos subsídios para o aperfeiçoá-lo. Em nosso trabalho aperfeiçoamos o método proposto, reescrevendo e adicionando características para torná-lo compatível com uma classificação de testes utilizada pela comunidade. O método também foi melhorado para suportar especificações estruturadas em vários componentes, utilizar informações sobre o comportamento da operação durante a criação de casos de teste e utilizar novos critérios de cobertura. Além disso, implementamos uma ferramenta para automatizá-lo e o submetemos a estudos de caso mais complexos