2011 Fiscal Year Annual Research Report
クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法
| Project/Area Number |
23240003
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (A)
|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
ARTHO Cyrille 独立行政法人産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
横山 重俊 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (10600968)
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (60443199)
|
|---|
| Keywords | 仕様記述・仕様検証 / ソフトウェアモデル検査 / クラウドコンピューティング |
|---|
| Research Abstract |
研究実施計画に記載のテーマに関して進捗を述べる．
(1) マスタースレーブモデル検査方式に関しては，その動作原理を定式化し，基本的な性質 (健全性) の証明，および他方式に対する時間・空間性能の机上比較等の検討を行った．性能に関しては，最も一般の場合には状態数の増加が確認されたため，現実のアプリケーションが持つ特有の性質に着目した最適化方式を考案し，この方式が健全性を保つ条件を確定した．対象ミドルウェアの検証のためにはnative peer等の整備が必要であることから，プロトタイプの作成は優先度を下げることとし，今後は定式化のために置いた仮定 (同期通信)の妥当性確認と仮定の除去の方向を目指す．
(2) native peer クラスライブラリの構成に関しては，当初計画通り，java.nio パッケージに対応するように構築を行った．既存の部分的実装を検討した結果，クラスによってまちまちな方法がとられていることが判明したため，既存ブロック入出力をラップする層で，ペンディング入力の読込を整数型選択生成器で行う方式を一貫して用いるように方針のもとですすめ，次項目で必要な範囲のnative peer クラス群を実装できた．あわせて，本方式による実装で探索可能なパターンの定式化も行った．
(3) 既存ツールによるミドルウェアソフトの検証は，ZooKeeper コンポーネントを主対象とすることとした．クラウド基盤全般にわたってサーバ間の協調動作を制御する，並行動作による競合に関連の深いコンポーネントであるからである．既存テストセットによるテストで意味のない結果が大半を占めたことを受け，テストセットをモデル検査目的に合うように改変した．このテスト結果に基づき，今後，検証モデルの改造を行っていく．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究の進展に伴って得られた知見から，当初計画に対して軌道修正を行ったが，その修正に対してはほぼ想定通りの進捗となっている．Zookeeperへの適用に関しては既存テストセットに関する見込み違いから遅れが生じたが，3ヶ月の延長によって予定のテストを完了している．
|
| Strategy for Future Research Activity |
本年度に行った，ZooKeeperコンポーネントを対象とした既存ツールの適用実験の結果，2つの課題が明らかになった．(1) サーバプログラムに対する際の状態数制御については，一般的な手法の適用を試行するほか，ZooKeeperプログラムの特性を利用した方法，たとえばヒューリスティックの適用等を検討する．(2) 検証モデルにおいて，簡単化のために導入している接続パターン等の制限(サーバ・クライアントの同一プロセスでの混在) の問題は，プロセス区分を設けない実装とする方向で検討を行う．
|
