BTestBox: uma ferramenta de teste para implementações B

Detalhes bibliográficos
Ano de defesa: 2018
Autor(a) principal: Oliveira, Diego de Azevedo
Orientador(a): Deharbe, David Boris Paul
Banca de defesa: Não Informado pela instituição
Tipo de documento: Dissertação
Tipo de acesso: Acesso aberto
Idioma: por
Instituição de defesa: Não Informado pela instituição
Programa de Pós-Graduação: PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO
Departamento: Não Informado pela instituição
País: Brasil
Palavras-chave em Português:
Área do conhecimento CNPq:
Link de acesso: https://repositorio.ufrn.br/jspui/handle/123456789/25489
Resumo: Softwares precisam ser seguros e corretos. Partindo desse pressuposto, novas tecnologias e técnicas são desenvolvidas para comprovar as competências de um programa. Essa necessidade de segurança se torna mais relevante ao tratar de softwares que atuam em sistemas críticos, como os sistemas ferroviário e aeroviário. A utilização de métodos formais na construção de software busca solucionar o problema. Ao utilizar o método formal B através da plataforma Atelier-B, e após provar os componentes de um projeto é necessária a tradução para a linguagem desejada. Essa tradução ocorre por meio de tradutores e compiladores B. Habitualmente, o processo de compilação em compiladores maduros é seguro, porém não estão completamente livres de falhas e eventualmente erros são encontrados. Ao expandir essa afirmação para tradutores B é necessário cautela, uma vez que esses não são tão comuns e utilizados quanto compiladores que circulam há mais tempo no mercado. Testes de software podem ser utilizados para realizar a análise da tradução. Através de critérios de cobertura é possível inferir o nível de qualidade do software e facilitar a detecção de falhas. Realizar a checagem da cobertura e testes em software pode exigir bastante esforço e tempo, principalmente ao serem realizados manualmente. Para sanar essa demanda, a ferramenta BTestBox visa analisar, de maneira automática, a cobertura atingida por implementações B desenvolvidas através do Atelier-B. BTestBox também testa automaticamente as traduções feitas a partir de implementações B. Para isso, BTestBox utiliza os casos de teste gerados para a verificação de cobertura e compara os valores esperados de saída com os encontrados após a tradução. O processo feito por BTestBox é todo automático e pode ser utilizado a partir do Atelier-B via instalação de plugin com uma interface simples. Essa dissertação apresenta a ferramenta BTestBox. BTestBox foi testado através de pequenas implementações B com os elementos gramaticais possíveis da linguagem B. BTestBox apresenta funcionalidade e vantagens para programadores que utilizam o método formal B.