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: a testing tool for B implementations

PALAVRAS-CHAVES:

B-Method, Software Test, Tool, Atelier-B, Code Coverage.

PÁGINAS: 71
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
RESUMO:

Software needs to be safe and correct. From that assumption, new technologies and techniques
are developed to prove the competencies of a program. This safety necessity is more
relevant when considering critical systems, such as railways and avionics systems. The use
of formal methods in the construction of software tries to solve this problem. When using B
in Atelier-B, after proving the components of a project is necessary to translate to the desired
language. This translation occurs using B translators and compilers. Usually, the process of
compilation is safe when done by mature compilers, although they are not free of errors and
eventually bugs are found. Expanding this affirmation to B translators demands caution, since
they are not used such as compilers that have more market time. Software testing may solve and
be used to perform the analyses of the translated code. Through coverage criteria is possible
to infer the level of quality of a software and detect bugs. To achieve the coverage check and
test the software is hard and time-consuming, mainly if done manually. To adress this demand,
the BTestBox tool aims to analyze, automatically, the coverage reached for B implementations
built through Atelier-B. BTestBox also automatically tests the translation from B implementations.
For this, BTestBox uses the same test case generated to verify the coverage and compare
the output expected values with the values found in the translation. This process made by
BTestBox is fully automatic and may be used from Atelier-B interface through a plugin with
easy interface.
This thesis proposal presents the tool BTestBox. The tool is the implementation of the
ideas proposed in the previous paragraph. BTestBox was tested with small B implementations
with all possible elements from B language. BTestBox presents various functionalities and
advantages to developers that use the B-Method.

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