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

共 7 条

[1] BROWNE MC, 1987, LECT NOTES COMPUT SC, V249, P256
[2] Clarke EM, 2009, COMMUN ACM, V52, P75, DOI 10.1145/1592761.1592781
[3] Clarke EM, 1999, MODEL CHECKING, P1
[4] Pasareanu Corina S., 2010, Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, ser. ASE'10, Antwerp, P179, DOI [DOI 10.1145/1858996.1859035, 10.1145/1858996.1859035]
[5] Model checking C source code for embedded systems
Bastian Schlich
Stefan Kowalewski
[J]. International Journal on Software Tools for Technology Transfer, 2009, 11 (3) : 187 - 202
[6] Application of static analyses for state-space reduction to the microcontroller binary code
Schlich, Bastian
Brauer, Joerg
Kowalewski, Stefan
[J]. SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (02) : 100 - 118
[7] Model Checking of Software for Microcontrollers
Schlich, Bastian
[J]. ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2010, 9 (04)

← 1 →