| 研究課題/領域番号 |
18K11239
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報通信学系, 教授 (70263506)
|
|---|
| 研究分担者 |
櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| キーワード | ソフトウェアモデル検査 / 組込みアセンブリプログラム |
|---|
| 研究実績の概要 |
H30年度は、以下の手法，理論およびそのツールを開発した．
１．以下の手法と理論を開発した：組込みソフトウェアのハードウェアとの相互作用およびタイミング制約を検証するために，アセンブリプログラムの変数値，スタックやアドレスばかりでなく，命令の実行時間を含めて，時間Kripke 構造（＝組込みソフトウェアの形式的意味モデル）を開発した．さらに，アセンブリプログラムを時間Kripke 構造へ変換する手法を開発した．また，リアルタイム安全性などの検証性質をリアルタイム時相論理で記述した．また，述語抽象化ベースのSMT抽象化手法，SMT抽象モデル検査手法，SMTベースの抽象化精錬手法を開発した．
２．以下のツールを開発した：述語抽象化手法をベースに，SMT 述語抽象化器とSMT 抽象モデル検査器を開発した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
H30年度は、上記の手法，理論およびそのツールを開発した．その成果を以下に発表した．
Yajun Wu, Satoshi Yamane:Model Checking of Embedded Systems Using RTCTL While Generating Timed Kripke Structure. IEEE COMPSAC (1) 2018: 257.
Hiromu Kamide, Kosuke Uemura, Satoshi Yamane:Model Check of Real-time Property of Embedded Assembly Program Using CEGAR. IEEE COMPSAC (1) 2018: 799-800.
|
| 今後の研究の推進方策 |
今後はSMT 反例解器及びSMT Interpolation による抽象化精錬器を開発して，SMTベースの抽象化精錬型のソフトウェアモデル検査器を実現する．
さらに，実用レベルの事例により，計算機実験を行い，提案手法の有効性を実証する．
また，その成果を国際会議及びジャーナルに投稿する．
|
| 次年度使用額が生じた理由 |
研究分担者の消耗品が少額で済んだので、次年度に回します。
|
