| 研究課題/領域番号 |
20300006
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
山本 光晴 千葉大学, 大学院・理学研究科, 准教授 (00291295)
|
|---|
| 研究分担者 |
萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
アルト シリル 独立行政法人産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任准教授 (60443199)
高橋 孝一 独立行政法人産業技術総合研究所, 情報技術研究部門, 情報戦略グループ長 (40357372)
|
|---|
| 研究期間 (年度) |
2008 – 2010
|
| 研究課題ステータス |
完了 (2010年度)
|
| 配分額 *注記 |
11,310千円 (直接経費: 8,700千円、間接経費: 2,610千円)
2010年度: 3,640千円 (直接経費: 2,800千円、間接経費: 840千円)
2009年度: 3,640千円 (直接経費: 2,800千円、間接経費: 840千円)
2008年度: 4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
|
|---|
| キーワード | モデル検査 / 仮想計算機 / チェックポインティング |
|---|
| 研究概要 |
状態の系統的・網羅的探索でプログラムの正当性を検証するモデル検査という手法がある。これをネットワークアプリケーションに適用するため、通信を含んだ形でプログラムの実行を遡るバックトラッキングを実装し、Javaプログラムのモデル検査器Java PathFinderの拡張の形で組み込んだ。通信を含むバックトラッキングは、通信相手のプログラムを実行状態の保存・復元が可能なチェックポインティング環境で動作させ、さらに通信接続の保存・復元のために独自の伝達層を用いて通信をすることで実現されている。
|
