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 条
  • [31] Model checking embedded and real time systems
    Larsen, Kim G.
    WODES' 08: PROCEEDINGS OF THE 9TH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS, 2008, : 260 - 260
  • [32] Incremental bounded model checking for embedded software
    Schrammel, Peter
    Kroening, Daniel
    Brain, Martin
    Martins, Ruben
    Teige, Tino
    Bienmueller, Tom
    FORMAL ASPECTS OF COMPUTING, 2017, 29 (05) : 911 - 931
  • [33] Model checking embedded adaptive cruise controllers
    Nenchev, Vladislav
    ROBOTICS AND AUTONOMOUS SYSTEMS, 2023, 167
  • [34] Model Checking Higher-Order Programs
    Kobayashi, Naoki
    JOURNAL OF THE ACM, 2013, 60 (03)
  • [35] LTL model checking for communicating concurrent programs
    Adrien Pommellet
    Tayssir Touili
    Innovations in Systems and Software Engineering, 2020, 16 : 161 - 179
  • [36] Heuristic model checking for Java']Java programs
    Groce, A
    Visser, W
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 242 - 245
  • [37] Abstracting Strings for Model Checking of C Programs
    Lauko, Henrich
    Olliaro, Martina
    Cortesi, Agostino
    Rockai, Petr
    APPLIED SCIENCES-BASEL, 2020, 10 (21): : 1 - 33
  • [38] Abstraction-based model checking programs
    Qian, Junyan
    Xu, Baowen
    Zhang, Yingzhou
    Journal of Computational Information Systems, 2007, 3 (02): : 675 - 682
  • [39] Tools and techniques for model checking networked programs
    Artho, Cyrille
    Leungwattanakit, Watcharin
    Hagiya, Masami
    Tanabe, Yoshinori
    PROCEEDINGS OF NINTH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, ARTIFICIAL INTELLIGENCE, NETWORKING AND PARALLEL/DISTRIBUTED COMPUTING, 2008, : 852 - +
  • [40] Model checking programs with Java']Java PathFinder
    Visser, W
    Mehlitz, P
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2005, 3639 : 27 - 27
12345