2012 Fiscal Year Annual Research Report
分散チェックポインティングを用いたネットワークアプリケーションのモデル検査
| Project/Area Number |
23300004
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩谷 昌己 東京大学, 情報理工学系研究科, 教授 (30156252)
ARTHO Cyrille 独立行政法人産業技術総合研究所, セキュアシステム研究部門, 研究員 (30462831)
田辺 良則 国立情報学研究所, アーキテクチャ科学系, 特任教授 (60443199)
|
|---|
| Project Period (FY) |
2011-04-01 – 2014-03-31
|
| Keywords | モデル検査 / チェックポインティング |
|---|
| Research Abstract |
本年度は、我々がモデル検査器の基盤として用いているJava PathFinderがネットワークAPIとして使用するモデルクラスとして、ノンブロッキングI/Oを含むJava.nioクラスの実装のコア部分をほぼ完成させた。我々の先行研究課題「仮想計算機によるコミュニケーションバックトラッキングとモデル検査への応用」では、モデルクラスとしてJava.ioクラスの実装を与えていたが、より多くのネットワークアプリケーションに対する検証を可能とするためには、ノンブロッキングI/Oへの対応が不可欠となる。この結果は本課題とメンバーが重なっている別課題「クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法」の基盤ともなる。
ソフトウェアについては、以下の2つを作成した。1つ目はJava PathFinderの環境をまるごと仮想環境として提供するもので、利用者が複数のソフトウェアをインストールする手間を省くのみならず、利用者側の環境の差異によらず、統一的・標準的な検証環境を提供するのに役立つ。2つ目は仮想環境を利用した分散チェックポインティングをモデル検査以外に応用したものであり、ネットワークアプリケーションに対してネットワーク切断などの稀なイベントを意図的に発生させて、正しくそれらに対処できているかを確かめるためのツールである。
また本年度は我々の先行研究課題および本課題の途中経過における成果をまとめた雑誌論文を提出し、現在査読者からのコメントに従って修正中である。残念ながら今年度は受理された論文が無かったが、来年度にこの雑誌論文および上記ソフトウェアに関連する論文が受理されることを目指している。
研究協力者 ヴァイテル・フランツ (千葉大学)
研究協力者 ポッター・リチャード (東京大学)
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
ソフトウェアの実装についてはほぼ予定通りに進んでいる。論文については今年度は受理されたものが無かったが、査読コメントからするとあと一歩というところであったように思われる。来年度は受理されなかったものの改訂版や、研究実績の概要で述べた、現在修正中の雑誌論文の出版を目指しており、今年度はそのための蓄積であったと考えられる。
|
| Strategy for Future Research Activity |
来年度は最終年度であるため、本課題の成果をソフトウェア・論文の両面でまとめ、公開することに特に重点を置く。さらに特にソフトウェア面での成果を、本課題とメンバーが重なっている別課題「クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法」に反映させることを念頭に置く。
研究計画の変更や研究を遂行する上での問題点は特段無い。
|
