1 |
BMCLua: Metodologia para Verificação de Códigos Lua utilizando Bounded Model CheckingJanuário, Francisco de Assis Pereira 01 April 2015 (has links)
Submitted by Kamila Costa (kamilavasconceloscosta@gmail.com) on 2015-08-03T12:38:15Z
No. of bitstreams: 2
Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5)
ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-08-04T15:34:24Z (GMT) No. of bitstreams: 2
Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5)
ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-08-04T15:38:25Z (GMT) No. of bitstreams: 2
Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5)
ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Made available in DSpace on 2015-08-04T15:38:25Z (GMT). No. of bitstreams: 2
Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5)
ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5)
Previous issue date: 2015-04-01 / CNPq - Conselho Nacional de Desenvolvimento Científico e Tecnológico / The development of programs written in Lua programming language, which is largely
used in applications for digital TV and games, can cause errors, deadlocks, arithmetic overflow,
and division by zero. This work aims to propose a methodology for checking programs written
in Lua programming language using the Efficient SMT-Based Context-BoundedModel Checker
(ESBMC) tool, which represents the state-of-the-art context-bounded model checker. It is used
for ANSI-C/C++ programs and has the ability to verify array out-of-bounds, division by zero,
and user-defined assertions. The proposed approach consists in translating programs written
in Lua to an intermediate language, which are further verified by ESBMC. The translator is
developed with the ANTLR (ANother Tool for Language Recognition) tool, which is used for
developing the lexer and parser, based on the Lua language grammar. This work is motivated by
the need for extending the benefits of bounded model checking, based on satisfiability modulotheories, to programs written in Lua programming language. The experimental results show that the proposed methodology can be very effective, regarding model checking (safety) of Luaprogramming language properties. / O desenvolvimento de programas escritos na linguagem de programação Lua, que é
muito utilizada em aplicações para TV digital e jogos, pode gerar erros, deadlocks, estouro
aritmético e divisão por zero. Este trabalho tem como objetivo propor uma metodologia de
verificação para programas escritos na linguagem de programação Lua usando a ferramenta
Efficient SMT-Based Context-Bounded Model Checker (ESBMC), que representa o estado da
arte em verificação de modelos de contexto limitado. O ESBMC é aplicado a programas embarcados
ANSI-C/C++ e possui a capacidade de verificar estouro de limites de vetores, divisão
por zero e assertivas definidas pelo usuário. A abordagem proposta consiste na tradução de
programas escritos em Lua para uma linguagem intermediária, que é posteriormente verificada
pelo ESBMC. O tradutor foi desenvolvido com a ferramenta ANTLR (do inglês “ANother Tool
for Language Recognition”), que é utilizada na construção de analisadores léxicos e sintáticos,
a partir da gramática da linguagem Lua. Este trabalho é motivado pela necessidade de se
estender os benefícios da verificação de modelos, baseada nas teorias de satisfatibilidade, a programas
escritos na linguagem de programação Lua. Os resultados experimentais mostram que
a metodologia proposta pode ser muito eficaz, no que diz respeito à verificação de propriedades
(segurança) da linguagem de programação Lua.
|
2 |
Verificação e comprovação de erros em códigos C usando bounded model checkerRocha, Herbert Oliveira 04 February 2011 (has links)
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.
|
Page generated in 0.0691 seconds