Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-10-11T20:48:07Z
No. of bitstreams: 1
ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-10-14T00:17:49Z (GMT) No. of bitstreams: 1
ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) / Made available in DSpace on 2016-10-14T00:17:49Z (GMT). No. of bitstreams: 1
ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5)
Previous issue date: 2016-04-14 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES) / Sistemas de software esta?o presentes em grande parte das nossas vidas atualmente e, mais do que nunca, eles requerem um alto ni?vel de confiabilidade. Existem va?rias te?cnicas de Ver- ificac?a?o e Validac?a?o (V&V) de software que se preocupam com controle de qualidade, segu- ranc?a, robustez e confiabilidade; as mais conhecidas sa?o Testes de Software e Me?todos For- mais. Me?todos formais e testes sa?o te?cnicas que podem se complementar. Enquanto me?to- dos formais prove?em mecanismos confia?veis para raciocinar sobre o sistema em um ni?vel mais abstrato, te?cnicas de teste ainda sa?o necessa?rias para uma validac?a?o mais profunda e sa?o frenquentemente requeridas por orga?os de certificac?a?o. Levando isto em considerac?a?o, BETA prove? uma abordagem de testes baseada em modelos para o Me?todo B, suportada por uma ferramenta, que e? capaz de gerar testes de unidade a partir de ma?quinas abstratas B. Nesta tese de doutorado apresentamos melhorias realizadas em BETA e novos estudos de caso realizados para avalia?-la. Dentre as melhorias, integramos crite?rios de cobertura lo?gicos a? abordagem, revisamos os crite?rios de cobertura baseados em espac?o de entrada que ja? eram suportados e aperfeic?oamos as u?ltimas etapas do processo de gerac?a?o de testes. A abordagem agora suporta a gerac?a?o automa?tica de dados para os ora?culos e prea?mbulos para os casos de teste; ela tambe?m possui uma funcionalidade para concretizac?a?o dos da- dos de teste e um mo?dulo para gerar scripts de teste executa?veis automaticamente. Outro objetivo desta tese foi realizar estudos de caso mais complexos utilizando BETA e avaliar a qualidade dos casos de teste que a abordagem produz. Estes estudos de caso foram os primeiros a avaliar o processo de gerac?a?o de testes por completo, desde a especificac?a?o dos casos de teste ate? a sua implementac?a?o e execuc?a?o. Em nossos u?ltimos experimentos, analisamos a qualidade dos casos de teste gerados por BETA, considerando cada crite?rio de cobertura suportado, utilizando me?tricas de cobertuda de co?digo como cobertura de in- struc?o?es e ramificac?o?es. Tambe?m utilizamos testes de mutac?a?o para avaliar a capacidade dos casos de teste de detectar faltas na implementac?a?o dos modelos. O resultados obtidos foram promissores mostrando que BETA e? capaz de detectar faltas introduzidas por progra- madores ou geradores de co?digo e que a abordagem pode obter bons resultados de cobertura para a implementac?a?o de um sistema baseado em modelos B. / Software systems are a big part of our lives and, more than ever, they require a high level of
reliability. There are many software Verification and Validation (V&V) techniques that are
concerned with quality control, security, robustness, and reliability; the most widely known
are Software Testing and Formal Methods. Formal methods and testing are techniques that
can complement each other. While formal methods provide sound mechanisms to reason
about the system at a more abstract level, testing techniques are still necessary for a more
in-depth validation of the system and are often required by certification standards. Taking
this into consideration, BETA provides a tool-supported, model-based testing approach for
the B Method that is capable of generating unit tests from abstract B machines. In this thesis,
we present improvements made in the BETA approach and tool, and new cases studies
used to evaluate them. Among these improvements, we integrated logical coverage criteria
into the approach, reviewed the input space criteria that was already supported, and enhanced
the final steps of the test generation process. The approach now has support for
automatic generation of oracle data and test case preambles, it has a feature for test data
concretization, and a module that automatically generates executable test scripts. Another
objective of this thesis was to perform more complex case studies using BETA and assess the
quality of the test cases it produces. These case studies were the first to evaluate the test
generation process as a whole, from test case design to implementation and execution. In
our last experiments, we assessed the quality of the test cases generated by BETA, considering
each coverage criteria it supports, using code coverage metrics such as statement and
branch coverage. We also used mutation testing to evaluate the ability of the generated test
cases to identify faults in the model?s implementation. The results obtained were promising,
showing that BETA is capable of detecting faults introduced by a programmer or code
generation tool and that it can achieve good coverage results for a system?s implementation
based on a B model.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/21417 |
| Date | 14 April 2016 |
| Creators | Matos, Ernesto Cid Brasil de |
| Contributors | 82573611787, http://lattes.cnpq.br/2363575151206774, Oliveira, Marcel Vin?cius Medeiros, 02386943488, http://lattes.cnpq.br/1756952696097255, Mota, Alexandre Cabral, 73547735491, http://lattes.cnpq.br/2794026545404598, Machado, Patricia Duarte de Lima, 67455069472, http://lattes.cnpq.br/2495918356675019, Leuschel, Michael, Moreira, Anamaria Martins |
| Publisher | PROGRAMA DE P?S-GRADUA??O EM SISTEMAS E COMPUTA??O, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0044 seconds