BTestBox: uma ferramenta de teste para implementações B
Software needs to be safe and run smoothly. From that assumption, new technologies and techniques are developed to test the quality of a program. This is more relevant when developing critical systems, such as railways and avionics control systems. Formal methods try to adress this need. When usi...
Na minha lista:
| Autor principal: | |
|---|---|
| Outros Autores: | |
| Formato: | Dissertação |
| Idioma: | por |
| Publicado em: |
Brasil
|
| Assuntos: | |
| Endereço do item: | https://repositorio.ufrn.br/jspui/handle/123456789/25489 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
| Resumo: | Software needs to be safe and run smoothly. From that assumption, new technologies and
techniques are developed to test the quality of a program. This is more relevant when developing
critical systems, such as railways and avionics control systems. Formal methods try
to adress this need. When using B in Atelier-B, after proving the components of a project is
necessary to translate to the desired language, a translation is made by using B translators and
compilers. Usually, the process of compilation is safe when perfomed by mature compilers
although they are not free of errors and bugs often crop up. The same reliability is not always
observed in B translators since they have been on the market for less time. Software testing
may solve and be used to perform the analyses of the translated code. From coverage criteria,
it is possible to infer quality of a piece of software and detect bugs. This process is hard and
time-consuming, mainly if it is perfomed manually. To address this problem, the BTestBox
tool aims to analyze automatically the coverage of 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 is fully automatic and may be started
from Atelier-B with a plugin. This thesis presents the tool BTestBox. The tool is a solution to the problems exposed in
the previous paragraph. BTestBox was tested with small B implementations and all gramatical
elements from B language. It offers various functionalities and advantages to developers that
use the B-Method. |
|---|