Banca de QUALIFICAÇÃO: DIEGO DE AZEVEDO OLIVEIRA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : DIEGO DE AZEVEDO OLIVEIRA
DATA : 20/06/2017
HORA: 09:00
LOCAL: DIMAp-Auditório II
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: 53
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 aviário. A utilização de métodos formais na construção de software busca solucionar o problema. Porém, mesmo desenvolvendo o software com o método formal B, entidades reguladoras demandam certificados que requisitam a utilização de testes de software e a comprovação da cobertura de código, por exemplo o certificado DO-178B exigido pela Administração Federal de Aviação (Federal Aviation Administration - FAA) que exige a cobertura MC/DC. Realizar a checagem da cobertura e teste de software podem exigir bastante esforço e tempo, principalmente ao serem realizadas 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. Infelizmente, 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ária cautela, uma vez que esses não são tão comuns e utilizados quanto compiladores que circulam a mais tempo no mercado. Mais uma vez, testes de software podem ser utilizados para realizar a análise da tradução. BTestBox também têm essa funcionalidade e testa automaticamente a tradução 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 plugin com uma interface simples.
Essa proposta de dissertação apresenta a ferramenta BTestBox. Até então, a ferramenta foi testada através de pequenas implementações B com todos os elementos possíveis da linguagem B. Os testes das traduções foram realizados utilizando o tradutor C4B. Infelizmente, até o estado atual esse é o único tradutor para o qual os testes foram implementados porém pode ser expandido para outros tradutores. BTestBox apresenta ampla possível funcionalidade e vantagens para programadores que utilizam o método formal B.


MEMBROS DA BANCA:
Presidente - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1258224 - ANAMARIA MARTINS MOREIRA
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Notícia cadastrada em: 16/06/2017 10:08
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa03-producao.info.ufrn.br.sigaa03-producao