| 研究課題/領域番号 |
15K00093
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| 研究分担者 |
櫻井 孝平 金沢大学, 電子情報学系, 助教 (80597021)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 組込みアセンブリプログラム / ソフトウェアモデル検査 / 抽象化精錬 / SMT / プログラム解析 |
|---|
| 研究実績の概要 |
平成27年度は以下を行った。
（１）アセンブリプログラムから検証モデル（Kripke構造）を構築する際に、状態爆発を抑制するために、以下の手法を提案して実証した。
①動的プログラム解析により、クロックサイクルを考慮した正確なモデルを構築する手法を提案した。これにより、タイマー割り込み処理の削減とクロックに矛盾した処理の削除を実現した。また、正確なモデル構築により、反例が発生しないために、正確な検証が実現できる。
②さらに、モデル構築の際に、ビット列の抽象化を行い、必要なときのみ精錬を行い、具体化する手法を提案した。これにより、状態爆発を抑制できた。
③さらに、モデル構築とモデル検査とを交互に行う手法を構築した。これにより、完全なモデルを構築しなくとも検証結果が得られる場合があり、規模の大きなアセンブリプログラムを検証できる場合が多いことを確認した。
（２）大規模アセンブリプログラムを検証するために、抽象化精錬（CEGAR）とSMTモデル検査を融合する手法を開発して、実装中である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
動的プログラム解析とビット列抽象化精錬により、アセンブリプログラムからクロックサイクルを含む最小なモデルを構築する手法を開発して、実装して実証できた。さらに、新たに、モデル構築とモデル検査を同時に行いながら、検証する手法を提案して、大規模プログラムの検証に効果があることを実証した。
また、大規模アセンブリプログラムを検証するために、抽象化精錬（CEGAR）とSMTモデル検査を融合する手法を開発して実装中である。
|
| 今後の研究の推進方策 |
現在、抽象化精錬（CEGAR）とSMTモデル検査を融合する手法を開発して実装中であり、本年度中にに、アセンブリプログラムに適した検証システムを構築する予定である。
さらに今後、Interpolationとresolutionを組み込んで、精錬述語の自動生成と検証の高度化を行う予定である。
|
| 次年度使用額が生じた理由 |
予定よりも旅費が安くなり、15700円が残った。
|
| 次年度使用額の使用計画 |
分担者の櫻井が15700円でコンピュータやネットワークの消耗品を購入する。
その他は、山根が旅費とその他（論文別刷）で使用する。
|
