研究課題
本年度の成果は、1)チェックポインティング機構の検討と採用2)Java Path Finder拡張としてのキャッシュ層実装の公開3)国際会議等での発表 に大別される。本研究の目的は、a)仮想計算機技術を拡張・発展させることにより、プログラムの実行を遡る「バックトラッキング」を、通信を含むネットワークアプリケーションにおいても可能にすることb)上記のバックトラッキングをソフトウェアモデル検査に応用し、ネットワークアプリケーションの効率的な検証を可能にすることであった。本課題の計画当初は仮想計算機機構を用いてモデル検査器を実装することを考えていた。しかし、今年度までの調査により、チェックポインティング機構のみに注力したシステムを用いても、本質的な部分は共通でかつより効率が良いバックトラッキング実装が得られる見込みが出てきた。よって、今年度からチェックポインティング機構に注力したシステムを用いた実装を行っており、これを来年度も継続する予定である。ネットワークアプリケーションのモデル検査を可能にするキャッシュ層については前年度から継続して実装を行っており、今年度はこれをNASAで開発されているモデル検査器Java Path Finder (JPF)の拡張として公開した。既にJPFのリポジトリに含まれており、またJava archiveファイルとしてNASAのページからダウンロード可能となっている。公開されているものにはまだバックトラッキング機構が含まれていないが、これを完成させることが来年度の課題となる。連携研究者東京大学大学院情報理工学系研究科田辺良則連携研究者産業技術総合研究所企画本部高橋孝一研究協力者東京大学大学院情報理工学系研究科レオンワタナキットワチャリン
すべて 2010 2009 その他
すべて 雑誌論文 (4件) (うち査読あり 4件) 学会発表 (1件) 備考 (1件)
DIPES 2010 : IFIP Conference on Distributed and Parallel Embedded Systems (掲載確定)
31st International Conference on Software Engineering, Companion Volume
ページ: 409-410
First NASA Formal Methods Symposium, NASA Conference Publication
ページ: 106-110
24th IEEE/ACM International Conference on Automated Software Engineering
ページ: 447-458
http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache
