• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2011 Fiscal Year Annual Research Report

クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法

Research Project

Project/Area Number 23240003
Research Category

Grant-in-Aid for Scientific Research (A)

Research InstitutionThe 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) 検証モデルにおいて,簡単化のために導入している接続パターン等の制限(サーバ・クライアントの同一プロセスでの混在) の問題は,プロセス区分を設けない実装とする方向で検討を行う.

  • Research Products

    (10 results)

All 2011 Other

All Journal Article (3 results) (of which Peer Reviewed: 3 results) Presentation (7 results)

  • [Journal Article] Model Checking Distributed Systems by Combining Caching and Process Checkpointing2011

    • Author(s)
      W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto
    • Journal Title

      Proc. 26th Int. Conf. on Automated Software Engineering (ASE 2011)

      Volume: 1 Pages: 103-112

    • DOI

      10.1109/ASE.2011.6100043

    • Peer Reviewed
  • [Journal Article] Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications2011

    • Author(s)
      Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, Masami Hagiya
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 7041 Pages: 350-365

    • DOI

      10.1007/978-3-642-24690-6_24

    • Peer Reviewed
  • [Journal Article] edubase Cloud: An Open-source Cloud Platform for Cloud Engineers2011

    • Author(s)
      Nobukazu Yoshioka, Shigetoshi Yokoyama, Yoshionori Tanabe, Shinichi Honiden
    • Journal Title

      SECLOUD '11 Proceedings of the 2nd International Workshop on Software Engineering for Cloud Computing

      Volume: 1 Pages: 73-73

    • Peer Reviewed
  • [Presentation] Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications2011

    • Author(s)
      Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, Masami Hagiya
    • Organizer
      9th International Conference of Software Engineering and Formal Methods, SEFM 2011
    • Place of Presentation
      Montevideo, Uruguay
    • Year and Date
      20111114-20111118
  • [Presentation] Model Checking Distributed Systems by Combining Caching and Process Checkpointing2011

    • Author(s)
      W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto
    • Organizer
      26th Int. Conf. on Automated Software Engineering (ASE 2011)
    • Place of Presentation
      Oread, Lawrence, Kan, USA
    • Year and Date
      20111106-20111112
  • [Presentation] ネットワークアプリケーションのマスター・スレーブ方式モデル検査アルゴリズムについて2011

    • Author(s)
      田辺 良則, Cyriile Artho, Watcharin Leungwattanakit, 山本 光晴, 萩谷 昌己
    • Organizer
      日本ソフトウェア科学会第28回大会
    • Place of Presentation
      沖縄産業支援センター,沖縄県那覇市
    • Year and Date
      20110927-20110929
  • [Presentation] edubase Cloud: An Open-source Cloud Platform for Cloud Engineers

    • Author(s)
      Nobukazu Yoshioka, Shigetoshi Yokoyama, Yoshionori Tanabe, Shinichi Honiden
    • Organizer
      2nd International Workshop on Software Engineering for Cloud Computing
    • Place of Presentation
      Waikiki, Honolulu, Hawaii, USA
  • [Presentation] Analysis of networked software

    • Author(s)
      Cyrille Artho
    • Organizer
      第4回新世代ネットワークおよび将来インターネットに関する日欧シンポジウム
    • Place of Presentation
      TKP東京駅八重洲カンファレンスセンター (東京都)
  • [Presentation] Analysis of networked and cloud computing software

    • Author(s)
      Cyrille Artho
    • Organizer
      International Workshop on Embedded Security of System and Software (IWESSS'12)
    • Place of Presentation
      National University of Singapore (シンガポール)
  • [Presentation] Analysis of networked and cloud computing software

    • Author(s)
      Cyrille Artho
    • Organizer
      第2回ソフトウェアと検証のワークショップ
    • Place of Presentation
      産業技術総合研究所 (兵庫県)

URL: 

Published: 2014-07-24  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi