Verificação e comprovação de erros em códigos C usando bounded model checker

Rocha, Herbert Oliveira; http://lattes.cnpq.br/2284500318304899

Dissertação

Verificação e comprovação de erros em códigos C usando bounded model checker

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 i...

ver descrição completa

Autor principal:	Rocha, Herbert Oliveira
Outros Autores:	http://lattes.cnpq.br/2284500318304899
Grau:	Dissertação
Idioma:	por
Publicado em:	Universidade Federal do Amazonas 2015
Assuntos:	Model checking Bounded model checker Propriedades de segurança Contra-exemplos Comprovação de Erros Model checking Bounded modelchecker Safety properties Counterexamples Proving errors CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
Acesso em linha:	http://tede.ufam.edu.br/handle/tede/2965

id	oai:https:--tede.ufam.edu.br-handle-:tede-2965
recordtype	dspace
spelling	oai:https:--tede.ufam.edu.br-handle-:tede-29652016-05-25T05:03:07Z Verificação e comprovação de erros em códigos C usando bounded model checker Rocha, Herbert Oliveira Barreto, Raimundo da Silva http://lattes.cnpq.br/2284500318304899 http://lattes.cnpq.br/1132672107627968 Model checking Bounded model checker Propriedades de segurança Contra-exemplos Comprovação de Erros Model checking Bounded modelchecker Safety properties Counterexamples Proving errors CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO 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. 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. CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior 2015-04-11T14:03:20Z 2013-07-25 2011-02-04 Dissertaçã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. http://tede.ufam.edu.br/handle/tede/2965 por Acesso Aberto application/pdf Universidade Federal do Amazonas Instituto de Computação BR UFAM Programa de Pós-graduação em Informática
institution	TEDE - Universidade Federal do Amazonas
collection	TEDE-UFAM
language	por
topic	Model checking Bounded model checker Propriedades de segurança Contra-exemplos Comprovação de Erros Model checking Bounded modelchecker Safety properties Counterexamples Proving errors CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
spellingShingle	Model checking Bounded model checker Propriedades de segurança Contra-exemplos Comprovação de Erros Model checking Bounded modelchecker Safety properties Counterexamples Proving errors CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO Rocha, Herbert Oliveira Verificação e comprovação de erros em códigos C usando bounded model checker
topic_facet	Model checking Bounded model checker Propriedades de segurança Contra-exemplos Comprovação de Erros Model checking Bounded modelchecker Safety properties Counterexamples Proving errors CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
description	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.
author_additional	Barreto, Raimundo da Silva
author_additionalStr	Barreto, Raimundo da Silva
format	Dissertação
author	Rocha, Herbert Oliveira
author2	http://lattes.cnpq.br/2284500318304899
author2Str	http://lattes.cnpq.br/2284500318304899
title	Verificação e comprovação de erros em códigos C usando bounded model checker
title_short	Verificação e comprovação de erros em códigos C usando bounded model checker
title_full	Verificação e comprovação de erros em códigos C usando bounded model checker
title_fullStr	Verificação e comprovação de erros em códigos C usando bounded model checker
title_full_unstemmed	Verificação e comprovação de erros em códigos C usando bounded model checker
title_sort	verificação e comprovação de erros em códigos c usando bounded model checker
publisher	Universidade Federal do Amazonas
publishDate	2015
url	http://tede.ufam.edu.br/handle/tede/2965
_version_	1831969079071604736
score	11.753896

Verificação e comprovação de erros em códigos C usando bounded model checker

Registros relacionados