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

2019 年度 実施状況報告書

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

研究課題

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

研究代表者

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

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

組込みアセンブリプログラムを対象として、アセンブリプログラムのリアルタイム性を検証できる、以下のソフトウェアモデル検査の理論、技術と手法を開発して、そのプロトタイプを実現して、それらの有効性を部分的に実証した。

1.【時間Kripke構造の自動生成】:組込みアセンブリプログラムから、リアルタイム性を含む時間Kripke構造を自動生成する手法及び時間Kripke構造自動生成システムを開発した。その自動生成システムは、Javaプログラム3000行程度で実装できて、アセンブリプログラムから時間Kripke構造を自動生成する機能を有する。ここで、各アセンブリ命令の実行クロック数を時間Kripke構造の各状態に付与して、リアルタイム性の記述を実現している。
2.【述語抽象化精錬】:述語抽象化とその精錬の理論を用いて、以下のような時間Kripke構造をソフトウェアモデル検査する手法を開発した。(1)述語を用いて、抽象化された時間Kripke構造を生成して、抽象モデル検査を行う。(2)(a)(1)で反例がなければ検証性質を満たすと判定して検証は終了する。(b)(1)で反例があれば、その反例が偽反例かどうかを判定して、(b-1)偽反例でなければ、検証性質を満たすと判定して検証は終了する。(b-2)偽反例であれば、偽反例を起こす状態列から、自動的にInterpolationを用いて、精錬述語を自動生成する。(3)(2)で生成した精錬述語を用いて、(1)の抽象化された時間Kripke構造を精錬して、(1)に戻り、(1)と(2)を繰り返す。
Java言語とSMT/SAT prover Z3により、以上の述語抽象化精錬によるモデル検査のプロトタイプを部分的に実装した。部分的ではあるが、組込みアセンブリプログラムのリアルタイム性の検証を実現して、開発した理論、技術と手法の妥当性と有効性を実証した。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

組込みアセンブリプログラムを対象として、リアルタイム性のソフトウェアモデル検査の理論、技術と手法を開発した。そして、そのプロトタイプを開発して、部分的に、開発した理論、技術と手法の有効性が実証できた。

今後の研究の推進方策

ソフトウェアモデル検査のプロトタイプを実現できたが、SMT検証の部分で未完成なものがある。
最後の1年間では、SMT検証の部分を完成させて、完全なソフトウェアモデル検査器を開発して、実用的なに例で実証実験を行う。
さらに、実用化するために、必要な機能を洗い出して、次の科研申請の準備をする。

次年度使用額が生じた理由

論文掲載料及び成果発表のための出張経費。

  • 研究成果

    (4件)

すべて 2020 2019

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

  • [雑誌論文] 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

    • 査読あり / オープンアクセス
  • [雑誌論文] Lazy Abstractionと精練を用いた組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査2020

    • 著者名/発表者名
      上出広夢、山根智
    • 雑誌名

      2019年冬のLAシンポジュム

      巻: 印刷中 ページ: 1-5

  • [雑誌論文] SMT-Based Bounded Model Checking of Embedded Assembly Program with Interruptions2019

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

      2019 IEEE Intl Conf on Dependable, Autonomic and Secure Computing

      巻: 17 ページ: 633-639

    • DOI

      10.1109/DASC/PiCom/CBDCom/CyberSciTech.2019.00120

    • 査読あり
  • [雑誌論文] Deductive Verification Method of Real-Time Safety Properties for Embedded Assembly Programs2019

    • 著者名/発表者名
      Satoshi Yamane
    • 雑誌名

      Electronics

      巻: 8(10) ページ: 1-16

    • DOI

      10.3390/electronics8101163

    • 査読あり

URL: 

公開日: 2021-01-27  

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

Powered by NII kakenhi