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.
| Identifer | oai:union.ndltd.org:IBICT/oai:http://localhost:tede/4539 |
| Date | 01 April 2015 |
| Creators | Januário, Francisco de Assis Pereira |
| Contributors | Cordeiro, Lucas Carvalho, Lima Filho, Eddie Batista de, Cordeiro, Lucas Carvalho, Silva Júnior, Waldir Sabino da, Dias Neto, Arilo Claudio |
| Publisher | Universidade Federal do Amazonas, Programa de Pós-graduação em Engenharia Elétrica, UFAM, Brasil, Faculdade de Tecnologia |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| 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 | -161377036298529205, 600, 600, -5930111888266832212 |
Page generated in 0.0018 seconds