Made available in DSpace on 2015-04-11T14:03:20Z (GMT). No. of bitstreams: 1
HERBERT OLIVEIRA.pdf: 512075 bytes, checksum: acc5d05442df938abdfa025f9db23367 (MD5)
Previous issue date: 2011-02-04 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The use of computer-based systems in several domains has increased significantly over
the last years, one of the main challenges in software development of these systems
is to ensure the correctness and reliability of these. So that software verification now
plays an important role in ensuring the overall product quality, aimed mainly the
characteristics of predictability and reliability. In the context of software verification,
with respect to the use of model checking technique, Bounded Model Checkers have
already been applied to discover subtle errors in actual systems projects, contributing
effectively in this verification process. The value of the counterexample and safety
properties generated by Bounded Model Checkers to create test case and to debug
these systems is widely recognized. When a Bounded Model Checking (BMC) finds
an error it produces a counterexample. Thus, the value of counterexamples to debug
software systems is widely recognized in the state-of-the-practice. However, BMCs
often produce counterexamples that are either large or difficult to be understood and
manipulated mainly because of both the software size and the values chosen by the
respective solver. In this work we aim to demonstrate and analyze the use of formal
methods (through using the model checking technique) in the process of developing
programs in C language, exploring the features already provided by the model checking
as the counterexample and the identification and verification of safety properties. In
view of this we present two approaches: (i) we describe a method to integrate the
bounded model checker ESBMC with the CUnit framework. This method aims to
extract the safety properties generated by ESBMC to generate automatically test cases
using the rich set of assertions provided by the CUnit framework and (ii) a method aims
to automate the collection and manipulation of counterexamples in order to instantiate
the analised C program for proving the root cause of the identified error. Such methods
may be seen as a complementary technique for the verification performed by BMCs.
We show the effectiveness of our proposed method over publicly available benchmarks
of C programs. / A utilização de sistemas baseados em computador em diversos domínios aumentou
significativamente nos últimos anos. Um dos principais desafios no desenvolvimento
de software de sistemas críticos é a garantia da sua correção e confiabilidade. Desta
forma, a verificação de software exerce um papel importante para assegurar a qualidade
geral do produto, visando principalmente características como previsibilidade e confiabilidade.
No contexto de verificação de software, os Bounded Model Checkers estão
sendo utilizados para descobrir erros sutis em projetos de sistemas de software atuais,
contribuindo eficazmente neste processo de verificação. O valor dos contra-exemplos e
propriedades de segurança gerados pelo Bounded Model Checkers para criar casos de
testes e para a depuração de sistemas é amplamente reconhecido. Quando um Bounded
Model Checking (BMC) encontra um erro ele produz um contra-exemplo. Assim,
o valor dos contra-exemplos para depuração de software é amplamente reconhecido no
estado da prática. Entretanto, os BMCs frequentemente produzem contra-exemplos
que são grandes ou difíceis de entender ou manipular, principalmente devido ao tamanho
do software e valores escolhidos pelo solucionador de satisfabilidade. Neste
trabalho visamos demonstrar e analisar o uso de método formal (através da técnica
model checking) no processo de desenvolvimento de programas na linguagem C, explorando
as características já providas pelo model checking como o contra-exemplo e a
identificação e verificação de propriedades de segurança. Em face disto apresentamos
duas abordagens: (i) descrevemos um método para integrar o Bounded Model Checker
ESBMC como o framework de teste unitário CUnit, este método visa extrair as
propriedades geradas pelo ESBMC para gerar automaticamente casos de teste usando
o rico conjunto de assertivas providas pelo framework CUnit e (ii) um método que
visa automatizar a coleta e manipulação dos contra-exemplos, de modo a instanciar o
programa C analisado, para comprovar a causa raiz do erro identificado. Tais métodos
podem ser vistos como um método complementar para a verificação efetuada pelos
BMCs. Demonstramos a eficácia dos métodos propostos sobre benchmarks públicos de
código C.
| Identifer | oai:union.ndltd.org:IBICT/oai:http://localhost:tede/2965 |
| Date | 04 February 2011 |
| Creators | Rocha, Herbert Oliveira |
| Contributors | Barreto, Raimundo da Silva |
| Publisher | Universidade Federal do Amazonas, Programa de Pós-graduação em Informática, UFAM, BR, Instituto de Computação |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| 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, 600, 1052477850274827528 |
Page generated in 0.0027 seconds