Uma Ferramenta para Geração de Testes de Unidade a partir de Especificações B
Métodos Formais; Testes de Software; Método B; Testes de Unidade.
O Método B é um método para especificação e desenvolvimento formal de sistemas. No Método B, especificações de um sistema são feitas através de máquinas B. Estas máquinas utilizam conceitos de teoria de conjuntos, lógica de primeira ordem e aritmética inteira, para definir máquinas de estado abstratas que representam o comportamento do sistema. Apesar de permitir que sistemas sejam matematicamente verificados, métodos formais não são suficientes para garantir que um sistema esteja livre de erros. Técnicas de teste de software são necessárias para complementá-los e prover mais segurança ao processo de desenvolvimento. Este trabalho tem como objetivo desenvolver uma ferramenta para geração automática de testes de unidade a partir especificações B. O método de geração de casos de teste que será utilizado pela ferramenta foi previamente definido por Fernanda Souza (2010), aluna do PPgSC. Utilizando informações do invariante de uma máquina B e pré-condições de uma operação, ele é capaz de gerar casos de testes positivos e negativos para uma operação do sistema, através de técnicas de particionamento de equivalência e análise de valor limite. Além de desenvolver uma ferramenta para a automação deste método, pretendemos formalizá-lo, realizar estudos de caso mais complexos e eventualmente ampliá-lo, adicionando novas estratégias de teste.