BTestBox: a testing tool for B implementations
B-Method, Software Test, Tool, Atelier-B, Code Coverage.
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.