| Summary: | Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-02T18:48:21Z
No. of bitstreams: 1
DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5) === Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-04T13:18:52Z (GMT) No. of bitstreams: 1
DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5) === Made available in DSpace on 2018-07-04T13:18:53Z (GMT). No. of bitstreams: 1
DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5)
Previous issue date: 2018-02-05 === 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 aeroviário. A utilização de métodos formais na construção de
software busca solucionar o problema. 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ário cautela, uma vez que esses não são tão comuns e utilizados quanto
compiladores que circulam há mais tempo no mercado. Testes de software podem ser utilizados
para realizar a análise da tradução. Através de critérios de cobertura é possível inferir o nível
de qualidade do software e facilitar a detecção de falhas. Realizar a checagem da cobertura
e testes em software pode exigir bastante esforço e tempo, principalmente ao serem realizados
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.
BTestBox também testa automaticamente as traduções 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 de plugin com
uma interface simples. Essa dissertação apresenta a ferramenta BTestBox. BTestBox foi testado através de pequenas implementações B com os elementos gramaticais possíveis da linguagem B. BTestBox
apresenta funcionalidade e vantagens para programadores que utilizam o método formal 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 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.
|
|---|
