Model Generation by the Exhaustive Search for Embedded Assembly Programs and Application to Model Checking

被引：0
|
作者：
Konoshita, Ryousuke [1 ]
Sakurai, Kouhei [1 ]
Yamane, Satoshi [1 ]
机构：
[1] Kanazawa Univ, Grad Sch Nat Sci Technol, Kanazawa, Ishikawa 9201192, Japan
来源：
2014 IEEE 3RD GLOBAL CONFERENCE ON CONSUMER ELECTRONICS (GCCE) | 2014年
关键词：
D O I：
暂无
中图分类号：
TM [电工技术]; TN [电子技术、通信技术];
学科分类号：
0808 ; 0809 ;
摘要：
Embedded systems have been widely used. Therefore, it is important to ensure the safety. Model checking is effective to ensure the safety for systems. We have developed Behavior Extractor to model the behavior of embedded assembly programs automatically. The model is used for model checking. In addition, we have introduced the undefined value to reduce the number of states.
引用
收藏
页码：699 / 702
页数：4
相关论文
共 50 条
  • [1] Model generation by the exhaustive search for embedded assembly programs and application to model checking
    20151000615754
    (1) Graduate School of Natural Science Technology, Kanazawa University, Japan, 1600, (Institute of Electrical and Electronics Engineers Inc., United States):
  • [2] An Efficient Reduction of Timer Interrupts for Model Checking of Embedded Assembly Programs
    Yamane, Satoshi
    Kriyama, Taro
    Wu, Yajun
    ELECTRONICS, 2024, 13 (02)
  • [3] Model Checking of Embedded Assembly Program Based on Simulation
    Yamane, Satoshi
    Konoshita, Ryosuke
    Kato, Tomonori
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2017, E100D (08): : 1819 - 1826
  • [4] Model Checking Driven Heuristic Search for Correct Programs
    Katz, Gal
    Peled, Doron
    MODEL CHECKING AND ARTIFICIAL INTELLIGENCE, 2009, 5348 : 122 - 131
  • [5] Delayed nondeterminism in model checking embedded systems assembly code
    Noll, Thomas
    Schlich, Bastian
    HARDWARE AND SOFTWARE: VERIFICATION AND TESTING, 2008, 4899 : 185 - 201
  • [6] Model Checking Programs
    Willem Visser
    Klaus Havelund
    Guillaume Brat
    SeungJoon Park
    Flavio Lerda
    Automated Software Engineering, 2003, 10 (2) : 203 - 232
  • [7] Model checking programs
    Visser, W
    Havelund, K
    Brat, G
    Park, SJ
    FIFTEENTH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2000, : 3 - 11
  • [8] Improving the model generation/checking interplay to enhance the evaluation of disjunctive programs
    Pfeifer, G
    LOGIC PROGRAMMING AND NONMONOTONIC REASONING, PROCEEDINGS, 2004, 2923 : 220 - 233
  • [9] Local Search in Model Checking
    Roscoe, A. W.
    Armstrong, P. J.
    Pragyesh
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2009, 5799 : 22 - +
  • [10] SMT-Based Bounded Model Checking of Embedded Assembly Program with Interruptions
    Uemura, Kousuke
    Yamane, Satoshi
    IEEE 17TH INT CONF ON DEPENDABLE, AUTONOM AND SECURE COMP / IEEE 17TH INT CONF ON PERVAS INTELLIGENCE AND COMP / IEEE 5TH INT CONF ON CLOUD AND BIG DATA COMP / IEEE 4TH CYBER SCIENCE AND TECHNOLOGY CONGRESS (DASC/PICOM/CBDCOM/CYBERSCITECH), 2019, : 633 - 639
12345