2016 Fiscal Year Research-status Report
革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証
| Project/Area Number |
15K00093
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
櫻井 孝平 金沢大学, 電子情報学系, 助教 (80597021)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 組込みアセンブリプログラム / ソフトウェアモデル検査 / プログラム解析 / SMT / 抽象化精錬 |
|---|
| Outline of Annual Research Achievements |
平成28年度は以下を行った。
（１）アセンブリプログラムから検証モデル（Kripke構造）を構築する際に、状態爆発を抑制して、モデル検査するシステムを実装して、多数の組込みアセンブリプログラムで計算機実験を行った。
また、その成果を英語ジャーナルに投稿して、条件付き採録であった。その論文の追加修正を行い、現在、最終判定待ちである。
（２）SMTソルバによるアセンブリプログラムの演繹的検証手法及びInterpolationによる精錬手法を改善中である。実装は平成29年度に行う予定である。その手法の特徴は以下である。①データ抽象化により、抽象モデルを構築する。②反例発見後は反例解析を行い、実反例があれば、CraigのInterpolationは効率が悪いので、RyndonのInterpolationを用いる。そのことを机上で実証した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
抽象化精錬において、反例発見後は反例解析を行い、実反例があれば、CraigのInterpolationで精錬述語を発見すると、効率が悪いことが判明した。そこで、それに代わる効率の良い方法を見つけるのに時間を要したためにやや遅れた。
しかし、RyndonのInterpolationという効率のよい方法を発見した。また、そのことを実例を用いて、机上で実証した。
|
| Strategy for Future Research Activity |
平成28年度までに、以下の手法を開発した。
①データ抽象化により、抽象モデルを構築する。
②反例発見後は反例解析を行い、実反例があれば、CraigのInterpolationは効率が悪いので、RyndonのInterpolationを用いる。
今後は、Uppsala大学のPhilipp RümmerのPrincess（Theorem Proving in First-Order Logic modulo Linear Integer Arithmetic）などの適当な定理証明系を利用して、検証システムを実装する。
|
