研究課題/領域番号 |
15K11989
|
研究種目 |
挑戦的萌芽研究
|
配分区分 | 基金 |
研究分野 |
数理情報学
|
研究機関 | 山形大学 |
研究代表者 |
平中 幸雄 山形大学, 大学院理工学研究科, 教授 (40134465)
|
連携研究者 |
武田 利浩 山形大学, 大学院理工学研究科, 助教 (90236472)
|
研究協力者 |
三浦 信一
稲船 哲也
門馬 悠太
|
研究期間 (年度) |
2015-04-01 – 2018-03-31
|
研究課題ステータス |
完了 (2017年度)
|
配分額 *注記 |
3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2017年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2016年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2015年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
キーワード | ソフトウェア安全性検証 / 逆方向シミュレーション / 逆実行モデル / 数値範囲分析 / シンボリック逆実行 / Java bytecode / 数値範囲分割 / 範囲分割逆モデル / Java機械語 / オーバフロー対応 / シミュレーション実行監視 / ケース分岐シミュレーション / GPU並列処理 / MapReduce分散処理 |
研究成果の概要 |
ソフトウェアの網羅的安全性検証を、逆方向シミュレーションを使って行う方法を研究した。具体的には、Java プログラムを対象に機械語に相当するバイトコードを逐次実行しながら、プログラム中のバグや誤動作要因を検出するシミュレータを実現した。逆方向シミュレーションを使うことで効率的に検出できるが、逆算方法として数値範囲分割方式とシンボリック分析方式を試み、それぞれの特質と課題に関する知見を得た。
|