Model checking of embedded assembly program based on simulation

• Yamane Satoshi

• Konoshita Ryosuke

• Kato Tomonori

• 山根 智

Abstract

金沢大学理工研究域電子情報学系

Embedded systems have been widely used. In addition, embedded systems have been gradually complicated. It is important to ensure the safety for embedded software by software model checking. We have developed a verification system for verifying embedded assembly programs. It generates exact Kripke structure by exhaustively and dynamically simulating assembly programs, and simultaneously verify it by model checking. In addition, we have introduced undefined values to reduce the number of states in order to avoid the state space explosion. Copyright © 2017 The Institute of Electronics, Information and Communication Engineers.

発行後6か月より出版社版

Journal

• IEICE Transactions on Information and Systems

  IEICE Transactions on Information and Systems E100D (8), 1819-1826, 2017-08-01

  電子情報通信学会 IEICE = The Institute of Electronics, Information and Communication Engineers

Keywords

• Embedded assembly program
• Model checking
• Simulation

Details

• CRID: 1390572174913658368
• NII Article ID: 120006374159
• NII Book ID: AA10826272
• ISSN: 09168532
• DOI: 10.24517/00049631
• Web Site: http://hdl.handle.net/2297/00049631
• Text Lang: en
• Data Source:
  • JaLC
  • IRDB
  • CiNii Articles