2012 Fiscal Year Annual Research Report
クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法
| Project/Area Number |
23240003
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
横山 重俊 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (10600968)
ARTHO Cyrille 独立行政法人産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (60443199)
|
|---|
| Project Period (FY) |
2011-04-01 – 2016-03-31
|
| Keywords | 仕様記述・仕様検証 / ソフトウェアモデル検査 / クラウドコンピューティング |
|---|
| Research Abstract |
研究実施計画に記載の項目に従って進捗を述べる．
(1) Java通信ライブラリのJPF対応では，各APIの意味を確定し，特にblocking IOによる実装を用いてnon-blocking IOの検証を行うことが妥当であることを確認した．その上で，従来のアドホックな実装を整理し，再設計・実装を行った．この検討を通して，新しいモデルベースのAPIテスト方式を着想し，プロトタイプツールを実装した．ツールの適用により，意味論と実装との合致をテスト可能であることが確認できた． 項目(2),(3) は，優先度を再検討した結果，ZooKeeper事例に基づいて探索空間の削減を行うこととした．これにより両項目を合わせての実施となった．(1)の結果を利用して，前年度のZooKeeper適用の際に適用不可能だったケースが適用可能となった．このうち状態空間の大きなものについて個別に探索空間削減を実現した． (4) マスタースレーブモデル検査は，予定通りプロトタイプ実装を行い，典型的なアプリケーションを用いて評価を行った．同期通信が理由となって，適用可能範囲が当初予想されたものよりも狭いことが認識されたため，非同期モデルへの拡張の検討を開始した． (5) ディプロイメントについては，クラウドコンピューティング環境において必要なソフトウェアを自動的に展開できるアーキテクチャ Dodai を考案した．これを用いることで検証時の環境と整合性を持つ環境を運用時に使用することが保証できる．
なお，項目(1)の実施中，複数接続方式設計に関して設計が不適切であったことが発見され，この修正に追加の4箇月を要した (繰越の要因) が，繰越期間の作業の結果，設計は適切に修正された．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
項目(1)の研究内容の進展にともない，年度なかばに新たな着想として，モデルベースAPIテスト方式が得られた．研究項目の優先度に再検討を加えた結果，この方式の可能性・将来性を重視して，当初掲げた研究実施項目(2),(3)の優先度を下げることにより，該当方式のツールプロトタイプ作成と評価を実施することとした．項目(2),(3)に関しては，他の実施項目の進捗に影響を与えない必要最小限の内容にとどまったが，その代わり，プロトタイプツールの仕様検討等に十分な時間をかけることができた．結果として項目(1)の実施にも資することとなった．優先度変更後の実施計画については，(下記を除き) ほぼ想定通りの進捗となっている．
なお，Java通信ライブラリの複数接続方式の設計に関して不適切な部分が発見された．影響範囲が大きかったために修正に長期間を要し，本研究課題を4箇月繰り越すこととなった．しかし，修正自体は計画通り終了し，また，広範に見直しを行った結果，Java通信ライブラリ対応全体の信頼性は向上したこともあり，妥当な計画変更であったと判断している．
|
| Strategy for Future Research Activity |
本年度開始したモデルベースAPIテスト方式は，今後の研究推進上重要な位置を占めることになると判断している．通信ライブラリのテストに利用できることはもちろんであるが，JPFが実現している網羅的な探索による検証との組み合わせによって検証を強化する研究方向も検討していく．
本年度実施した小事例への適用実験から，net-iocacheライブラリがサポートするプロトコルが，単純なクライアント-サーバ方式の，特定のモデルに限られていることに起因する問題点がいくつか確認された．peer-to-peer の構成や ftp などのアプリケーションレイヤのプロトコル，udp 等のトランスポートレイヤのプロトコル等を含め，適用できる通信モデルの増強進めていく必要がある．
|
