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

2014 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 23240003
Research InstitutionThe University of Tokyo

Principal Investigator

萩谷 昌己  東京大学, 情報理工学(系)研究科, 教授 (30156252)

Co-Investigator(Kenkyū-buntansha) 山本 光晴  千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
ARTHO Cyrille  独立行政法人産業技術総合研究所, 情報セキュリティセンター, 研究員 (30462831)
田辺 良則  国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (60443199)
Project Period (FY) 2011-04-01 – 2016-03-31
Keywords仕様記述・仕様検証 / ソフトウェアモデル検査 / クラウドコンピューティング
Outline of Annual Research Achievements

研究実施計画の項目に従って進捗を述べる.
(1) net-iocache v2.TCP通信に関しては,クライアント側の基本的な機能を完成させた.チャネル間依存関係に関しては,すべてのチャネルに依存関係があり得るとの仮定を置き,キャッシュは線形のものに限定し,プリフェッチも使用しないという前提で,本機能の設計,実装を行った.この範囲で正しく機能することが確認できている.
(2) モデルベーステストツールModbat.入力されたモデルからより多くのテストパスを効率的に生成するための改良を検討し,設計・実装を行った.特に,従来の同期式コールバックに加えて,非同期式コールバックを追加したことで,適用可能なアプリケーションを増すことに成功した.
(3) UDP検証.パケットの消失,重複,順序変更の3つの事象が非決定的に発生するプロトコルを解析するとの立場で研究を進めている.条件が無いと対象の遷移系の大きさが無限になってしまうので,遅延パケットの数と重複を発生させるパターンを限定 (パラメタで与える) して,遷移系を有限としたモデルを扱うこととした.この前提の下で,状態数に関する理論的な解析を行い,各パラメタが遷移系の大きさに与える影響を明らかにした.さらに,net-iocache v2 の上にUDP解析モジュールを実装し,主要なAPIに対応した.この実装を用いて,UDPによる通信を行うアプリケーションが持つ不具合を発見できることを実証した.
(4) JPF探索アルゴリズム (マスター・スレーブモデル検査).JPFのメイン探索エンジン変更の準備として,LTLモデル検査アルゴリズムのうちのNDFSの実装と,DFSベースのヒューリスティック探索機能の実装を行った.
(5) jpf-nas, nhandler連携.基本的な検討を行ったが,いずれについてもただちに実装可能な連携は難しいとの結論となった.しかし,検討の過程で明らかになった事項のいくつかは項目(1)の設計に反映させることができた.

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

2014年度は,項目(1)(3)に関して大きな進捗があった.項目(1)のチャネル相互の依存関係の考慮について,前年度までは単なる構想でしかなかった.いくつかの制限を置いた上とはいえ,実際に依存関係のあるチャネルを持つアプリケーションを対象とした実装ができたことで,完成に向けての具体的な計画を立てることが可能となった.項目(3)については,理論および実装の両面で,ほぼ最終的な形となったと言える.残りの(2),(4)についても,最終年度での完成が見通せる段階に達していると評価している.
項目(5)に関しては実績があまり無かったが,もともと試行するという位置づけの計画であり,連携相手のソフトウェアの完成度の問題もあったため,やむを得なかったと考える.一方で,この項目の検討を通して項目(1)の設計上の問題点が明らかになり,これを修正することができたので,検討自体は意義があったと評価できる.

Strategy for Future Research Activity

研究項目に関しては,昨年度の検討の結果棚上げとなった項目(5)を除いて,従来の項目を引き継いでいく.最終年度となるので,各項目に関して理論・実装の両面で現在得られている結果を参照しつつ検討の方向性を整理し,年度末に向けて各項目毎に成果をまとめることができるように研究を進めていく.
研究成果の広報,普及については,当研究課題の直接のターゲットが Java PathFinder をフレームワークとした検証ツールであることを踏まえ,開発・利用者コミュニティが研究成果を容易に利用できるようにするという観点から,ドキュメントの整備やスクリプトなどの利用ツールの整備を,優先度を上げて行っていく.

  • Research Products

    (11 results)

All 2015 2014

All Journal Article (5 results) (of which Acknowledgement Compliant: 2 results,  Peer Reviewed: 4 results) Presentation (6 results)

  • [Journal Article] A Knoppix-based demonstration environment for JPF2014

    • Author(s)
      Richard Potter, Cyrille Artho, Kuniyasu Suzaki, Masami Hagiya
    • Journal Title

      ACM SIGSOFT Software Engineering Notes

      Volume: 39 Pages: 1-5

    • DOI

      10.1145/2557833.2560574

    • Acknowledgement Compliant
  • [Journal Article] Software Model Checking of UDP-based Distributed Applications2014

    • Author(s)
      Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • Journal Title

      Proc. Second International Symposium on Computing and Networking

      Volume: 2014 Pages: 96-105

    • DOI

      10.1109/CANDAR.2014.66

    • Peer Reviewed
  • [Journal Article] Using Checkpointing and Virtualization for Fault Injection2014

    • Author(s)
      Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
    • Journal Title

      Proc. Second International Symposium on Computing and Networking

      Volume: 2014 Pages: 144-150

    • DOI

      10.1109/CANDAR.2014.45

    • Peer Reviewed / Acknowledgement Compliant
  • [Journal Article] モデル検査による設計検証2014

    • Author(s)
      吉岡信和,田辺良則,田原康之,長谷川哲夫,磯部祥尚
    • Journal Title

      コンピュータソフトウェア

      Volume: 31 Pages: 40-65

    • DOI

      10.11309/jssst.31.4_40

    • Peer Reviewed
  • [Journal Article] Scalaの並行プログラム検査における状態空間探索手法2014

    • Author(s)
      島田工,前澤悠太,鄭顕志,田辺良則,本位田真一
    • Journal Title

      第9回ソフトウェアエンジニアリングシンポジウム論文集

      Volume: 2014 Pages: 54-59

    • Peer Reviewed
  • [Presentation] 遷移のキャッシュを行うLTLモデル検査方式2015

    • Author(s)
      田辺良則
    • Organizer
      第17回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      道後プリンスホテル(愛媛県)
    • Year and Date
      2015-03-04 – 2015-03-06
  • [Presentation] ソフトウェアモデル検査におけるLTL検証の探索範囲限定手法による効率化2014

    • Author(s)
      前岡 淳, 田辺 良則, 石川 冬樹
    • Organizer
      第21回 ソフトウェア工学の基礎ワークショップ
    • Place of Presentation
      霧島国際ホテル (鹿児島県)
    • Year and Date
      2014-12-11 – 2014-12-13
  • [Presentation] Software Model Checking of UDP-based Distributed Applications2014

    • Author(s)
      Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • Organizer
      The Second International Symposium on Computing and Networking (CANDAR 2014)
    • Place of Presentation
      静岡県コンベンションアーツセンター (静岡県)
    • Year and Date
      2014-12-10 – 2014-12-12
  • [Presentation] Using Checkpointing and Virtualization for Fault Injection2014

    • Author(s)
      Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
    • Organizer
      The Second International Symposium on Computing and Networking (CANDAR 2014)
    • Place of Presentation
      静岡県コンベンションアーツセンター (静岡県)
    • Year and Date
      2014-12-10 – 2014-12-12
  • [Presentation] Model-based testing2014

    • Author(s)
      Cyrille Artho
    • Organizer
      Shonan Meeting 2014-16
    • Place of Presentation
      湘南国際村センター (神奈川県)
    • Year and Date
      2014-12-01 – 2014-12-04
  • [Presentation] Scalaの並行プログラム検査における状態空間探索手法2014

    • Author(s)
      島田工,前澤悠太,鄭顕志,田辺良則,本位田真一
    • Organizer
      第9回ソフトウェアエンジニアリングシンポジウム
    • Place of Presentation
      芝浦工業大学 (東京都)
    • Year and Date
      2014-09-01 – 2014-09-03

URL: 

Published: 2016-06-01  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi