2015 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 |
平成27年度は以下を行った。
（１）アセンブリプログラムから検証モデル（Kripke構造）を構築する際に、状態爆発を抑制するために、以下の手法を提案して実証した。
①動的プログラム解析により、クロックサイクルを考慮した正確なモデルを構築する手法を提案した。これにより、タイマー割り込み処理の削減とクロックに矛盾した処理の削除を実現した。また、正確なモデル構築により、反例が発生しないために、正確な検証が実現できる。
②さらに、モデル構築の際に、ビット列の抽象化を行い、必要なときのみ精錬を行い、具体化する手法を提案した。これにより、状態爆発を抑制できた。
③さらに、モデル構築とモデル検査とを交互に行う手法を構築した。これにより、完全なモデルを構築しなくとも検証結果が得られる場合があり、規模の大きなアセンブリプログラムを検証できる場合が多いことを確認した。
（２）大規模アセンブリプログラムを検証するために、抽象化精錬（CEGAR）とSMTモデル検査を融合する手法を開発して、実装中である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
動的プログラム解析とビット列抽象化精錬により、アセンブリプログラムからクロックサイクルを含む最小なモデルを構築する手法を開発して、実装して実証できた。さらに、新たに、モデル構築とモデル検査を同時に行いながら、検証する手法を提案して、大規模プログラムの検証に効果があることを実証した。
また、大規模アセンブリプログラムを検証するために、抽象化精錬（CEGAR）とSMTモデル検査を融合する手法を開発して実装中である。
|
| Strategy for Future Research Activity |
現在、抽象化精錬（CEGAR）とSMTモデル検査を融合する手法を開発して実装中であり、本年度中にに、アセンブリプログラムに適した検証システムを構築する予定である。
さらに今後、Interpolationとresolutionを組み込んで、精錬述語の自動生成と検証の高度化を行う予定である。
|
| Causes of Carryover |
予定よりも旅費が安くなり、15700円が残った。
|
| Expenditure Plan for Carryover Budget |
分担者の櫻井が15700円でコンピュータやネットワークの消耗品を購入する。
その他は、山根が旅費とその他（論文別刷）で使用する。
|
