BMCLua: Verification of Lua Programs in Digital TV Interactive Applications

被引：0
|
作者：
Januario, Francisco A. P. [1 ]
Cordeiro, Lucas C. [1 ]
de Lucena, Vicente F., Jr. [1 ]
de Lima Filho, Eddie B. [2 ]
机构：
[1] Univ Fed Amazonas, Manaus, Amazonas, Brazil
[2] Ind Pole Manaus CT PIM, Sci Technol & Innovat Ctr, Manaus, Amazonas, Brazil
来源：
2014 IEEE 3RD GLOBAL CONFERENCE ON CONSUMER ELECTRONICS (GCCE) | 2014年
关键词：
Digital TV; Model Checking;
D O I：
暂无
中图分类号：
TM [电工技术]; TN [电子技术、通信技术];
学科分类号：
0808 ; 0809 ;
摘要：
The present paper describes a novel scheme for checking for potential defects in Lua programs, by using Bounded Model Checking (BMC). Such an approach, called BMCLua, translates a Lua program into an ANSI-C one, which is then verified by the Efficient SMT-Based Bounded Model Checker (ESBMC). BMCLua is able to check for safety properties related to array bounds, division by zero, and user-specified assertions, in Lua programs. This paper marks the first application of BMC to Lua programs. The experimental results show that the performance of BMCLua is similar to that of ESBMC, in about 70% of the benchmarks used for evaluation.
引用
收藏
页码：707 / 708
页数：2
相关论文
共 50 条
  • [31] Personalized and mobile digital TV applications
    Chorianopoulos, Konstantinos
    [J]. MULTIMEDIA TOOLS AND APPLICATIONS, 2008, 36 (1-2) : 1 - 10
  • [32] Mechanical verification of interactive programs specified by use cases
    Claret, Guillaume
    Regis-Gianas, Yann
    [J]. 2015 IEEE/ACM 3RD FME WORKSHOP ON FORMAL METHODS IN SOFTWARE ENGINEERING, 2015, : 61 - 67
  • [33] Personalized and mobile digital TV applications
    Konstantinos Chorianopoulos
    [J]. Multimedia Tools and Applications, 2008, 36 : 1 - 10
  • [34] Exploiting smart spaces for interactive TV applications development
    Saleemi, M. Mohsin
    Lilius, Johan
    [J]. JOURNAL OF SUPERCOMPUTING, 2014, 70 (03): : 1200 - 1217
  • [35] Exploiting smart spaces for interactive TV applications development
    M. Mohsin Saleemi
    Johan Lilius
    [J]. The Journal of Supercomputing, 2014, 70 : 1200 - 1217
  • [36] A distributed platform for personalized advertising in digital interactive TV environments
    Athanasiadis, Erast
    Mitropoulos, Sarandis
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2010, 83 (08) : 1453 - 1469
  • [37] Distributed Personalization: Bridging Digital Islands in Museum and Interactive TV
    Aroyo, Lora
    [J]. ERCIM NEWS, 2008, (72): : 40 - 41
  • [38] Quality Verification of Digital TV Signals in a Production Line Environment
    Seixas, Paulo
    Levy, Pamela
    de Lima Filho, Eddie B.
    Caetano, Rogerio
    [J]. 2016 IEEE INTERNATIONAL SYMPOSIUM ON CONSUMER ELECTRONICS - 20TH IEEE ISCE, 2016, : 27 - 28
  • [39] A personalized TV Guide System An Approach to Interactive Digital Television
    de Avila, Paulo Muniz
    Zorzo, Sergio Donizetti
    [J]. 2009 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS (SMC 2009), VOLS 1-9, 2009, : 2122 - 2127
  • [40] OpenCL and parallel primitives for digital TV applications
    Cho, S. M.
    Im, D. W.
    Jang, O. Y.
    Song, H. J.
    Paulovicks, B. D.
    Sheinin, V.
    Yeo, H.
    [J]. IBM JOURNAL OF RESEARCH AND DEVELOPMENT, 2010, 54 (05)
12345