Submitted by Lúcia Brandão (lucia.elaine@live.com) on 2015-12-11T18:49:43Z
No. of bitstreams: 1
Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-19T14:41:05Z (GMT) No. of bitstreams: 1
Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-01-19T14:54:32Z (GMT) No. of bitstreams: 1
Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) / Made available in DSpace on 2016-01-19T14:54:32Z (GMT). No. of bitstreams: 1
Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5)
Previous issue date: 2015-07-03 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Oneofthemainchallenges insoftwaredevelopment istoensurethesafetyofthesoftwaresystems,
especially in critical embedded systems, such as aircraft or healthcare, where several constraints
(e.g., response time and data accuracy) must be met and measured in accordance with the user
requirements, otherwise a failure can lead to catastrophic situations. Thus, software verification
and testing techniques are essential items for the software development with quality, where such
techniques aim to confirm the user requirements, as well as, the predetermined behaviors for the
software.
In the software verification context, aiming the product quality, the formal verification technique
called model checking has been used to find subtle errors in actual projects of the software
systems. However, the use of the model checking technique presents some challenges such as
dealing with the model’s state explosion problem, integration with software testing environments
more familiar to designers, and handling counter-examples to reproduce the identified errors. In
order to deal with these problems, a possible solution is to explore the characteristics already
provided by the model checkers, e.g., verification of the safety properties and generation of
counter-examples. Exploring this set of characteristics, coupled with the use of program invariants
inference and a special kind of model checking, called Bounded Model Checking (BMC), this
thesis presents a set of methods to complement and enhance the scalability and accuracy of the
verification performed by Bounded Model Checkers. These methods adopted code transformation
techniques to explore the characteristics of Bounded Model Checkers to analyze the safety
properties and demonstrate errors in programs written inthe C programming language.
The methods presented in this thesis are: (1) The automatic generation and verification of the
test cases based on safety properties generated by a Bounded Model Checker for unit tests; (2)
Automating thecollection andmanipulation of thedatafrom thecounter-examples, todemonstrate
the main cause of the identified error; and (3) Adopting program invariants dynamically/statically
inferred from the analyzed program, to restrict the exploration of the states sets while performing
the verification by the BMC. This way, helping to improve the verification performed by a BMC,
related to assist in the verification and accuracy of results, by adoption of the program invariants.
The proposed approaches when used separately, provide additional options to the verification, and
interconnected, improving the code verification. Theexperimental results of theproposed methods
show to be efficient over public available benchmarks of C programs, finding errors not previously
found byother methods that are state-of-the-art. / Um dos principais desafios no desenvolvimento de software é garantir a funcionalidade dos
sistemas de software, especialmente em sistemas embarcados críticos, tais como aeronáutico ou
hospitalar, onde diversas restrições (por exemplo, tempo de resposta e precisão dos dados) devem
ser atendidas e mensuradas de acordo com os requisitos do usuário, caso contrário uma falha pode
conduzir a situações catastróficas. Logo, técnicas de verificação e teste de software são itens
indispensáveis para um desenvolvimento com qualidade, onde tais técnicas visam confirmar os
requisitos do usuário, bem como os comportamentos pré-estabelecidos para osoftware.
No contexto de verificação de software, visando à qualidade geral do produto, a técnica de
verificação formal model checking tem sido utilizada para descobrir erros sutis em projetos de
sistemas de software atuais. Contudo, a utilização da técnica model checking apresenta alguns
desafios, tais como, lidar com a explosão do espaço de estados do modelo, integração com outros
ambientes de testes mais familiares aos projetistas e tratamento e análise de contra-exemplos para
reprodução de erros. De modo a lidar com estes problemas, uma possível solução é explorar as
características já providas pelos model checkers, por exemplo, a verificação de propriedades de
segurança e geração de contra-exemplos. Explorando este conjunto de características, juntamente
com autilização dainferência deinvariantes eumtipo especial demodelchecking, denominado de
BoundedModelChecking (BMC),esta tese apresenta um conjunto de métodos para complementar
e aprimorar a escalabilidade e acurácia da verificação efetuada por Bounded Model Checkers.
Estes métodos utilizam técnicas de transformações de código para explorar as características de
Bounded Model Checkers, a fim de analisar propriedades de segurança e demonstrar erros em
códigos escritos na linguagem de programação C.
Os métodos apresentados nesta tese são: (1) A geração e verificação automática de casos de teste
baseado em propriedades de segurança geradas por um Bounded Model Checker para testes de
unidade; (2) Automatizar acoleta emanipulação das informações dos contra-exemplos, de modo a
demonstrar a causa principal do erro identificado; e (3) Utilização de invariantes
dinamicamente/estaticamente inferidas, a partir do programa analisado, para restringir a
exploração dos conjuntos de estados durante a execução da verificação pelo BMC. Desta forma,
ajudando no aprimoramento da verificação efetuada por um BMC, no que concerne em auxiliar a
sua verificação e na precisão dos resultados, pela utilização de invariantes de programas. As
abordagens propostas, quando utilizadas isoladamente, fornecem alternativas complementares a
verificação e, interligadas, aprimoram a verificação de código. Os resultados experimentais dos
métodos propostos demonstram ser eficientes sobre benchmarks públicos de programas em C,
encontrando defeitos não anteriormente encontrados por outros métodos que são estado-da-arte.
| Identifer | oai:union.ndltd.org:IBICT/oai:http://localhost:tede/4752 |
| Date | 03 July 2015 |
| Creators | Rocha, Herbert Oliveira |
| Contributors | Barreto, Raimundo da Silva, Cordeiro, Lucas Carvalho, Dias Neto, Arilo Claudio, Lettnin, Djones Vinicius, Becker, Leandro Buss |
| Publisher | Universidade Federal do Amazonas, Programa de Pós-graduação em Informática, UFAM, Brasil, Instituto de Computação |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFAM, instname:Universidade Federal do Amazonas, instacron:UFAM |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | -312656415484870643, 600 |
Page generated in 0.0022 seconds