2009 Fiscal Year Annual Research Report
仮想計算機によるコミュニケーションバックトラッキングとモデル検査への応用
| Project/Area Number |
20300006
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
山本 光晴 Chiba University, 大学院・理学研究科, 准教授 (00291295)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
アルト シリル 産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
|
|---|
| Keywords | モデル検査 / 仮想計算機 |
|---|
| Research Abstract |
本年度の成果は、1)チェックポインティング機構の検討と採用2)Java Path Finder拡張としてのキャッシュ層実装の公開3)国際会議等での発表 に大別される。
本研究の目的は、a)仮想計算機技術を拡張・発展させることにより、プログラムの実行を遡る「バックトラッキング」を、通信を含むネットワークアプリケーションにおいても可能にすることb)上記のバックトラッキングをソフトウェアモデル検査に応用し、ネットワークアプリケーションの効率的な検証を可能にすることであった。
本課題の計画当初は仮想計算機機構を用いてモデル検査器を実装することを考えていた。しかし、今年度までの調査により、チェックポインティング機構のみに注力したシステムを用いても、本質的な部分は共通でかつより効率が良いバックトラッキング実装が得られる見込みが出てきた。よって、今年度からチェックポインティング機構に注力したシステムを用いた実装を行っており、これを来年度も継続する予定である。
ネットワークアプリケーションのモデル検査を可能にするキャッシュ層については前年度から継続して実装を行っており、今年度はこれをNASAで開発されているモデル検査器Java Path Finder (JPF)の拡張として公開した。既にJPFのリポジトリに含まれており、またJava archiveファイルとしてNASAのページからダウンロード可能となっている。公開されているものにはまだバックトラッキング機構が含まれていないが、これを完成させることが来年度の課題となる。
連携研究者東京大学大学院情報理工学系研究科田辺良則
連携研究者産業技術総合研究所企画本部高橋孝一
研究協力者東京大学大学院情報理工学系研究科レオンワタナキットワチャリン
|
