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 条
  • [21] Model checking nonblocking MPI programs
    Siegel, Stephen F.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2007, 4349 : 44 - 58
  • [22] Model Checking Linear Programs with Arrays
    Armando, Alessandro
    Benerecetti, Massimo
    Mantovani, Jacopo
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (03) : 79 - 94
  • [23] Autotuning Parallel Programs by Model Checking
    Garanina, N. O.
    Gorlatch, S. P.
    AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2022, 56 (07) : 634 - 648
  • [24] Slicing concurrent programs for model checking
    Dong, Wei
    Wang, Ji
    Qi, Zhi-Chang
    Jisuanji Xuebao/Chinese Journal of Computers, 2003, 26 (03): : 266 - 274
  • [25] Bounded model checking of pointer programs
    Charatonik, W
    Georgieva, L
    Maier, P
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2005, 3634 : 397 - 412
  • [26] Automatic Test Case Generation by means of Model-Checking for Control Programs
    Kormann, B.
    Witsch, D.
    Vogel-Heuser, B.
    AUTOMATION 2010, 2010, : 473 - 476
  • [27] Automatic Test Cases Generation for C Written Programs Using Model Checking
    Gonzalez Lima, Daniset
    Gonzalez Torres, Raul E.
    Mejia Alvarez, Pedro
    2021 INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE AND COMPUTATIONAL INTELLIGENCE (CSCI 2021), 2021, : 1944 - 1950
  • [28] Mutation-Based Test Generation for PLC Embedded Software Using Model Checking
    Enoiu, Eduard P.
    Sundmark, Daniel
    Causevic, Adnan
    Feldt, Robert
    Pettersson, Paul
    TESTING SOFTWARE AND SYSTEMS, ICTSS 2016, 2016, 9976 : 155 - 171
  • [29] Modeling and testing embedded system by model checking
    Sun, Fuzhen
    Song, Dandan
    Liao, Lejian
    Li, Guoqiang
    International Journal of Advancements in Computing Technology, 2012, 4 (17) : 18 - 27
  • [30] Motivating Model Checking of Embedded Systems Software
    Reinbacher, Thomas
    Kramer, Michael
    Horauer, Martin
    Schlich, Bastian
    PROCEEDINGS OF 2008 IEEE/ASME INTERNATIONAL CONFERENCE ON MECHATRONIC AND EMBEDDED SYSTEMS AND APPLICATIONS, 2008, : 546 - +
12345