組込みアセンブラのSMT検証手法の提案と実装

• 竹下, 淳

• 小橋, 潤平

• 山根, 智

書誌事項

タイトル別名

• Verification of embedded software in Assembly code by SMT prover

抄録

本稿では，組込みアセンブリプログラムを対象とした 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.

収録刊行物

• 組込みシステムシンポジウム2012論文集

  組込みシステムシンポジウム2012論文集 2012 197-202, 2012-10-10

キーワード

• モデル検査

詳細情報

• CRID: 1050011097177997056
• NII論文ID: 170000072432
• Web Site: http://id.nii.ac.jp/1001/00086010/
• 本文言語コード: ja
• 資料種別: conference paper
• データソース種別:
  • IRDB
  • CiNii Articles