Métodos Formais; Teste de Software; Método B; Testes Baseados em Modelos.
Sistemas de software estão presentes em grande parte das nossas vidas atualmente e, mais do que nunca, eles requerem um alto nível de confiabilidade. Existem várias técnicas de Ver- ificação e Validação (V&V) de software que se preocupam com controle de qualidade, segu- rança, robustez e confiabilidade; as mais conhecidas são Testes de Software e Métodos For- mais. Métodos formais e testes são técnicas que podem se complementar. Enquanto méto- dos formais provêem mecanismos confiáveis para raciocinar sobre o sistema em um nível mais abstrato, técnicas de teste ainda são necessárias para uma validação mais profunda e são frenquentemente requeridas por orgãos de certificação. Levando isto em consideração, BETA provê uma abordagem de testes baseada em modelos para o Método B, suportada por uma ferramenta, que é capaz de gerar testes de unidade a partir de máquinas abstratas B. Nesta tese de doutorado apresentamos melhorias realizadas em BETA e novos estudos de caso realizados para avaliá-la. Dentre as melhorias, integramos critérios de cobertura lógicos à abordagem, revisamos os critérios de cobertura baseados em espaço de entrada que já eram suportados e aperfeiçoamos as últimas etapas do processo de geração de testes. A abordagem agora suporta a geração automática de dados para os oráculos e preâmbulos para os casos de teste; ela também possui uma funcionalidade para concretização dos da- dos de teste e um módulo para gerar scripts de teste executáveis automaticamente. Outro objetivo desta tese foi realizar estudos de caso mais complexos utilizando BETA e avaliar a qualidade dos casos de teste que a abordagem produz. Estes estudos de caso foram os primeiros a avaliar o processo de geração de testes por completo, desde a especificação dos casos de teste até a sua implementação e execução. Em nossos últimos experimentos, analisamos a qualidade dos casos de teste gerados por BETA, considerando cada critério de cobertura suportado, utilizando métricas de cobertuda de código como cobertura de in- struções e ramificações. Também utilizamos testes de mutação para avaliar a capacidade dos casos de teste de detectar faltas na implementação dos modelos. O resultados obtidos foram promissores mostrando que BETA é capaz de detectar faltas introduzidas por progra- madores ou geradores de código e que a abordagem pode obter bons resultados de cobertura para a implementação de um sistema baseado em modelos B.