2017 年度研究成果報告書

革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証

研究課題

研究課題/領域番号	15K00093
研究種目	基盤研究(C)
配分区分	基金
応募区分	一般
研究分野	ソフトウェア
研究機関	金沢大学
研究代表者	山根智金沢大学, 電子情報学系, 教授 (70263506)
研究分担者	櫻井孝平金沢大学, 電子情報学系, 助教 (80597021)
研究期間 (年度)	2015-04-01 – 2018-03-31
キーワード	ソフトウェアモデル検査 / 組込みアセンブリプログラム / 抽象化精錬 / ＳＭＴ / 定理証明
研究成果の概要	研究成果は以下の2つに大別できる．（1）動的プログラム解析の枝刈りと抽象化，実行時間見積もりによる最小なモデル構築器（アセンブリプログラムから割込み処理が埋め込まれた最小モデルを構築する）を作成した．（2）抽象化精錬(CEGAR)型ＳＭＴモデル検査手法を開発した．このモデル検査手法はＳＭＴによる述語抽象化、ＳＭＴ有界モデル検査、ＳＭＴによる反例解析器、ＳＭＴソルバによるInterpolationを用いた精錬述語の生成からなる．なお、ＳＭＴソルバとして、種々のInterpolationをサポートしているUppsala大学のPrincessを用いた．
自由記述の分野	ソフトウェア