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

PALAVRAS-CHAVES:

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

PÁGINAS: 53
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 shows more relevant when considering the critical system, such as the railway and aviary systems. The use of formal methods in the construction of the software tries to solve this problem. Although, even developing the software with the formal method B, regulation entities demand certificates that request the use of software testing and prove of code coverage, for example, the certificate DO-178B asked by the Federal Aviation Administration (FAA) that requires the MC/DC coverage.

To achieve the coverage check and test the software is hard and time-consuming, mainly if done manually. To suppress this demand, the BTestBox tool aims to analyze, automatically, the coverage reached for B implementations build through Atelier-B. Unfortunately, when using B over Atelier-B, after the proving the components of a project is necessary to translate to the desired language. This translation occurs due to 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 order caution, since they are not even common or used such as compilers that have more market time. Once again, software testing may solve and be used to perform the analyze of the translated code. BTestBox also does this function and automatically test the translation from B implementations. For this, BTestBox uses the same test case generated to verify the coverture 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. Until now, the tool was tested with little B implementations with all possible elements from B language. The tests of the translation were done using the C4B translator. Unfortunately, in the actual state, this is the only one translator that the test was done, but the tool shall support another translator in the future. BTestBox presents various functionalities and advantages to developers that use the B-Method.

MEMBROS DA BANCA:
Presidente - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1258224 - ANAMARIA MARTINS MOREIRA
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA