Verificação de Códigos Lua Utilizando BMCLua

Francisco de A. P. Januário, Lucas Cordeiro, Eddie B. L. Filho

DOI: 10.14209/sbrt.2013.199

Evento: XXXI Simpósio Brasileiro de Telecomunicações (SBrT2013)

Keywords: TV Digital Verificação de modelos Lua

Abstract

O presente artigo descreve uma abordagem de verificação de possíveis defeitos em códigos Lua, através da ferramenta Bounded Model Checker. Tal abordagem traduz código escrito em Lua para ANSI-C e o avalia através do Efficient SMT-Based Context-Bounded Model Checker (ESBMC), que é um verificador de modelos de contexto limitado para códigos 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. Este trabalho é motivado pela necessidade de se estender os benefícios da verificação de modelos, baseada nas teorias de satisfatibilidade, para códigos escritos na linguagem Lua. Os resultados apresentados, neste artigo, mostram a viabilidade da verificação de códigos Lua através da ferramenta ESBMC.

Download