組込みソフトウェアのアセンブラのSMT検証  [in Japanese] Verification of embedded software in Assembly code by SMT prover  [in Japanese]

Search this Article

Author(s)

Abstract

本稿では,組込みアセンブリプログラムを対象としたSMT有界モデル検査手法を以下のように提案する.(1)検証の前処理として,アセンブリプログラムをSSA形式に変換処理する.(2)アセンブリプログラムのSSA形式からSMT-LIBに変換してSMT有界モデル検査を行う.以上の検証手法をJavaで実装して実証実験を行った.

We propose the technique of Bounded Model Checking(BMC) for embedded assembly program. We use SMT solver for BMC. We also propose improvement of SSA conversion algorithm for assembly program and implement the Algorithm using Java language. Finally, we verify the simple assembly program's property of a real embedded robot system.

Journal

  • Technical report of IEICE. VLD

    Technical report of IEICE. VLD 112(114), 37-42, 2012-06-25

    The Institute of Electronics, Information and Communication Engineers

References:  16

Codes

  • NII Article ID (NAID)
    110009625716
  • NII NACSIS-CAT ID (NCID)
    AN10013323
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    0913-5685
  • NDL Article ID
    023872433
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS 
Page Top