• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2020 年度 実績報告書

組込みアセンブリプログラムのリアルタイム安全性のソフトウェアモデル検査手法の開発

研究課題

研究課題/領域番号 18K11239
研究機関金沢大学

研究代表者

山根 智  金沢大学, 電子情報通信学系, 教授 (70263506)

研究分担者 櫻井 孝平  金沢大学, 電子情報通信学系, 助教 (80597021)
研究期間 (年度) 2018-04-01 – 2021-03-31
キーワードソフトウェアモデル検査 / 組込みアセンブリプログラム / 時間Kripke構造 / SAT/SMT理論 / 抽象化精錬(CEGAR)
研究実績の概要

本研究では,これまでの研究成果をもとに,組込みアセンブリプログラムのリアルタイム安全性検証を実現するために,以下の分担(代表者 山根がモデル検査の理論実装,分担者 櫻井がプログラム解析)で,申請者らは前年度までに以下の成果を上げた。(①何を ②どのように ③どこまで明らかに)
(1)時間Kripke 構造により,アセンブリプログラムのハードウェアとの相互作用およびタイミング制約の形式的意味の定義(担当:山根)① アセンブリプログラムのハードウェアとの相互作用およびタイミング制約などの形式的意味を時間Kripke 構造で表現した.② アセンブリプログラムから時間Kripke 構造に変換して,さらに検証性質をリアルタイム時相論理で仕様記述した.③現実の組込みアセンブリプログラムの意味及びその検証性質が時間Kripke 構造及びリアルタイム時相論理で表現できることを,理論的及び実験的に明らかにした.

本年度は、上記の前年度の成果をもとに、以下の成果を上げた。
(2)アセンブリプログラムのソフトウェアモデル検査(担当:山根,櫻井,大学院生5 名)① アセンブリプログラムのソフトウェアモデル検査を開発した.② アセンブリプログムのプログラム解析及び述語抽象化からなるSMT 述語抽象化により,時間Kripke 構造の抽象化を行った(担当:櫻井,山根).③ 抽象時間Kripke 構造のSMT 述語抽象化,SMT 抽象モデル検査,SMT 反例解析,SMT Interpolation(担当:山根)により,組込みアセンブリプログラムのリアルタイム性の抽象化精錬のソフトウェアモデル検査手法を開発した.大学院生5 名と共同で,プロトタイプを実装して,現実の組込みソフトウェアのリアルタイム性の検証が行えることを明らかにした.

  • 研究成果

    (4件)

すべて 2020

すべて 雑誌論文 (4件) (うち査読あり 4件、 オープンアクセス 2件)

  • [雑誌論文] Model Checking of Real-Time Properties for Embedded Assembly Program Using Real-Time Temporal Logic RTCTL and Its Application to Real Microcontroller Software2020

    • 著者名/発表者名
      Yajun Wu, Satoshi Yamane
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: 103(4) ページ: 800-812

    • DOI

      10.1587/transinf.2019EDP7172

    • 査読あり / オープンアクセス
  • [雑誌論文] Comparative Experiment of SPIN and SMT in Model Checking of Embedded Assembly Program2020

    • 著者名/発表者名
      Satoshi Yamane, Kosuke Uemura
    • 雑誌名

      2020 IEEE 9th Global Conference on Consumer Electronics (GCCE)

      巻: 9 ページ: 54-57

    • DOI

      10.1109/GCCE50665.2020.9291772

    • 査読あり
  • [雑誌論文] Software Model Checking for Real-time Properties of Embedded Assembly Programs Based on Lazy Abstraction and Refinement2020

    • 著者名/発表者名
      Yajun Wu, Hiromu Kamide, Satoshi Yamane
    • 雑誌名

      2020 IEEE 9th Global Conference on Consumer Electronics (GCCE)

      巻: 9 ページ: 62-65

    • DOI

      10.1109/GCCE50665.2020.9291966

    • 査読あり
  • [雑誌論文] Verification Method of Safety Properties of Embedded Assembly Program by Combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions2020

    • 著者名/発表者名
      Satoshi Yamane, Junpei Kobashi, Kosuke Uemura
    • 雑誌名

      MDPI electronics

      巻: 9(7) ページ: 1-24

    • DOI

      10.3390/electronics9071060

    • 査読あり / オープンアクセス

URL: 

公開日: 2021-12-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi