O objetivo do BMCLua é estender as características de ESBMC, que é um verificador de modelos para software embarcado C/C++, para a linguagem de programação Lua. O verificador de modelo ESBMC é baseado em teorias do módulo da satisfação.O BMCLua é executado no sistema operacional Linux, que exige a instalação do software ESBMC e um interpretador Lua. Como o BMCLua é desenvolvido em Java, também é necessário a instalação do JRE para Linux. A versão atual do BMCLua verifica apenas um subconjunto das instruções de linguagem de programação Lua. Uma versão futura, que está sob o desenvolvimento, irá verificar todos os comandos, operadores e estruturas da linguagem de programação Lua.
Responsáveis
|
|
|
Redes Sociais