???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/2965
Tipo do documento: Dissertação
Título: Verificação e comprovação de erros em códigos C usando bounded model checker
Autor: Rocha, Herbert Oliveira 
Primeiro orientador: Barreto, Raimundo da Silva
Resumo: 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.
Abstract: 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.
Palavras-chave: Model checking
Bounded model checker
Propriedades de segurança
Contra-exemplos
Comprovação de Erros
Model checking
Bounded modelchecker
Safety properties
Counterexamples
Proving errors
Área(s) do CNPq: CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
Idioma: por
País: BR
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Instituto de Computação
Programa: Programa de Pós-graduação em Informática
Citação: ROCHA, Herbert Oliveira. Verificação e comprovação de erros em códigos C usando bounded model checker. 2011. 76 f. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas, Manaus, 2011.
Tipo de acesso: Acesso Aberto
URI: http://tede.ufam.edu.br/handle/tede/2965
Data de defesa: 4-Feb-2011
Appears in Collections:Mestrado em Informática

Files in This Item:
File Description SizeFormat 
HERBERT OLIVEIRA ROCHA.pdfDissertação500,32 kBAdobe PDFThumbnail

Download/Open Preview


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.