2010 Fiscal Year Annual Research Report
仮想計算機によるコミュニケーションバックトラッキングとモデル検査への応用
| Project/Area Number |
20300006
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
山本 光晴 千葉大学, 大学院・理学研究科, 准教授 (00291295)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
アルト シリル 産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任准教授 (60443199)
|
|---|
| Keywords | モデル検査 / 仮想計算機 / チェックポインティング |
|---|
| Research Abstract |
本年度の成果は、1)チェックポインティンク機構を利用したJava Path Finder拡張の実装と公開2)成果ヒ表に大別される。
本研究の目的は、a仮想計算機技術を拡張・発展させることにより、プログラムの実行を遡る「パックトラッキング」を、通信を含むネットワークアプリケーションにおいても可能にすることb)上記のパックトラッキングをソフトウェアモデル検査に応用し、ネットワークアプリケーションの効率的な検証を可能にすることであった。
前年度までの調査の結果を反映させ、パックトラッキングに仮想計算機ではなくチォックポインティグを利用するとうに設計を変更した。ネットワークアプリケーションにバックトラッキングを適用するには、通信相手の復元時に通信接続を回復させる必要かせあるが、我々がチェックポインティングに利用したMTCPは通信接続の回復に対応していない。そこで、独自にトランスポート層を実装することでこの問題を解決した。
研究成果はワークショップ等での発表に加え、実装をNASAで開発されているもでる検査器Java Path Finder (JPF)の拡張として公開しており、Java archiveファイルとしてNASAのページからダウンロード可能である。前年度はでに公開済みのものと比較して、本課題の主たる目的である通信を含むバックトラッキング機構が追加された。
本課題は今年度が最終年度である。本課題の成果では、検証対象のネットワークアプリケーションの通信相手として単一プロセスのアプリケーションしか利用できなかったが、平成23年度からの新課題において、本課題の成果をより発展させ、プロセスを動的に生成する通信相手や、複数プロセスからなる通信相手にも対応させる予定である。
研究協力者東京大学大学院情報理工学系研究科レオンワタナキットワチャリン
|
