Banca de DEFESA: DIEGO DE AZEVEDO OLIVEIRA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : DIEGO DE AZEVEDO OLIVEIRA
DATA : 05/02/2018
HORA: 08:00
LOCAL: Auditório I do DIMAp
TÍTULO:

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


PALAVRAS-CHAVES:

Método B, Teste de Software, Ferramenta, Atelier-B, Code Coverage.


PÁGINAS: 71
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 facilita a detecção de falhas. Realizar a checagem da cobertura
e testes em software podem 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 BTest-
Box é todo automático e pode ser utilizado a partir do Atelier-B via instalação de plugin com
uma interface simples.
Essa proposta de dissertação apresenta a ferramenta BTestBox. A ferramenta é a implementação
das ideias propostas no parágrafo anterior. BTestBox foi testado através de pequenas
implementações B com todos os elementos possíveis da linguagem B. BTestBox apresenta
funcionalidade e vantagens para programadores que utilizam o método formal B.


MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 2220777 - DAVID BORIS PAUL DEHARBE
Externo à Instituição - VALÉRIO GUTEMBERG DE MEDEIROS JUNIOR - IFRN
Notícia cadastrada em: 25/01/2018 10:17
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2019 - UFRN - sigaa07-producao.info.ufrn.br.sigaa07-producao