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

2015 Fiscal Year Annual Research Report

• Project/Area Number: 23240003
• Research Institution: The 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．(モデル検査器Java PathFinderでネットワークアプリケーションの検査を可能にする機構) 平成26年度に行った再設計に基づき，既存の部分的な実装をベースに，全体の実装を行った．v1に比較して，SUT (検証対象プログラム) に対する暗黙の仮定を減らすことが実現でき，また，粒度の異なる状態探索の方法が選択可能となった．v1との性能比較を実施し，多くの探索方式において，v1を上回る速度で検証が可能となることを確認した．事例研究の一環として，IoTで用いられるプロトコルであるMQTTクライアントに対してv2を利用したモデル検査を実施することで障害を検出した．MQTTプロトコルによる通信に関しても本手法が有効であることが確認できた．また，早期にバグを発見する手法であるSAMCの考え方をnet-iocacheに導入する実験にも成功した．本ライブラリの公開に関しては，すでに研究者・開発者に利用可能としていたが，文書やサンプルプログラムなどを整備することで，いっそう利用しやすくした．
(2) Modbat．(モデルベーステストツール) Hadoopにおけるプロセス協調実現機構であるZookeeperへのModbatの適用に取り組んだ．クライアントが非同期的な要求を行うことに伴う非決定性を扱うために，Modbatにモデル検査器を組み込むこととした．この機構により，すべての出力の可能性を扱うことが可能となり，妥当なモデルを構築することができた．
(3) UDP検証．平成26年度に，UDP通信を行うプログラムをJPFでモデル検査する方式を開発して得られた知見に基づき，UDPが許容する不確実性を分類し，各々の発現の程度に関する過程に応じてパケット数の評価を行った．すべてのパケットの組み合わせを生成する健全かつ完全なアルゴリズムを考案した．

Research Progress Status

27年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

27年度が最終年度であるため、記入しない。

Research Products

• [Journal Article] Guiding random test generation with program analysis (2016)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Journal Title: Proc Software Engineering 2016 Volume: 2016 Pages: 15-16
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] Cardinality of UDP Transmission Outcomes (2015)
  • Author(s): Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto
  • Journal Title: Proc 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications Volume: 2015 Pages: 120-134
  • DOI: 10.1007/978-3-319-25942-0_8
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Using Checkpointing and Virtualization for Fault Injection (2015)
  • Author(s): Cyrille Artho, Kuniyasu Suzaki, Masami Hagiya, Watcharin Leungwattanakit, Richard Potter, Eric Platon, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
  • Journal Title: International Journal of Networking and Computing Volume: 5 Pages: 347-372
  • DOI: 10.15803/ijnc.5.2_347
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Software Model Checking of UDP-based Distributed Applications (2015)
  • Author(s): Nazim Sebih, Masami Hagiya, Franz Weitl, Mitsuharu Yamamoto, Cyrille Artho, Yoshinori Tanabe
  • Journal Title: International Journal of Networking and Computing Volume: 5 Pages: 373-402
  • DOI: 10.15803/ijnc.5_2_373
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Model-Based Testing of Stateful APIs with Modbat (2015)
  • Author(s): Cyrille Artho, Martina Seidl, Quentin Gros, Eun-Hye Choi, Takashi Kitamura, Akira Mori, Rudolf Ramler, Yoriyuki Yamagata
  • Journal Title: Proc 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 2015 Pages: 858-863
  • DOI: 10.1109/ASE.2015.95
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] GRT: Program-Analysis-Guided Random Testing (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Journal Title: Proc 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 2015 Pages: 212-223
  • DOI: 10.1109/ASE.2015.49
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] GRT: An Automated Test Generator Using Orchestrated Program Analysis (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Journal Title: Proc 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 2015 Pages: 842-847
  • DOI: 10.1109/ASE.2015.102
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Domain-Specific Languages with Scala (2015)
  • Author(s): Cyrille Artho, Klaus Havelund, Rahul Kumar, Yoriyuki Yamagata
  • Journal Title: Proc 17th International Conference on Formal Engineering Methods Volume: 2015 Pages: 1-16
  • DOI: 10.1007/978-3-319-25423-4_1
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] GRT at the SBST 2015 Tool Competition (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
  • Journal Title: Proc 8th IEEE/ACM International Workshop on Search-Based Software Testing Volume: 2015 Pages: 48-51
  • DOI: 10.1109/SBST.2015.19
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] Depth-First Heuristic Search for Software Model Checking (2015)
  • Author(s): Jun Maeoka, Yoshinori Tanabe, Fuyuki Ishikawa
  • Journal Title: Proc 14th IEEE/ACIS International Conference on Computer and Information Science Volume: 2015 Pages: 75-96
  • DOI: 10.1007/978-3-319-23467-0_6
  • Peer Reviewed
• [Presentation] Precondition Coverage in Software Testing (2016)
  • Author(s): Cyrille Artho, Guillaume Rousset, Quentin Gros
  • Organizer: 1st International Workshop on Validating Software Tests
  • Place of Presentation: 大阪大学 (大阪府大阪市)
  • Year and Date: 2016-03-15 – 2016-03-15
  • Int'l Joint Research
• [Presentation] Classification of Randomly Generated Test Cases (2016)
  • Author(s): Cyrille Artho, Lei Ma
  • Organizer: 1st International Workshop on Validating Software Tests
  • Place of Presentation: 大阪大学 (大阪府大阪市)
  • Year and Date: 2016-03-15 – 2016-03-15
  • Int'l Joint Research
• [Presentation] Domain-Specific Languages with Scala (2015)
  • Author(s): Cyrille Artho, Klaus Havelund, Rahul Kumar, Yoriyuki Yamagata
  • Organizer: 17th International Conference on Formal Engineering Methods
  • Place of Presentation: パリ (フランス)
  • Year and Date: 2015-12-05 – 2015-12-05
  • Int'l Joint Research
• [Presentation] Model-Based Testing of Stateful APIs with Modbat (2015)
  • Author(s): Cyrille Artho, Martina Seidl, Quentin Gros, Eun-Hye Choi, Takashi Kitamura, Akira Mori, Rudolf Ramler, Yoriyuki Yamagata
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: リンカーン (米国)
  • Year and Date: 2015-11-13 – 2015-11-13
  • Int'l Joint Research
• [Presentation] GRT: An Automated Test Generator Using Orchestrated Program Analysis (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ram\ ler
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: リンカーン (米国)
  • Year and Date: 2015-11-12 – 2015-11-12
  • Int'l Joint Research
• [Presentation] GRT: Program-Analysis-Guided Random Testing (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: リンカーン (米国)
  • Year and Date: 2015-11-11 – 2015-11-11
  • Int'l Joint Research
• [Presentation] Cardinality of UDP Transmission Outcomes (2015)
  • Author(s): Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto
  • Organizer: 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications
  • Place of Presentation: 南京 (中国)
  • Year and Date: 2015-11-04 – 2015-11-04
  • Int'l Joint Research
• [Presentation] Depth-First Heuristic Search for Software Model Checking (2015)
  • Author(s): Jun Maeoka, Yoshinori Tanabe, Fuyuki Ishikawa
  • Organizer: 14th IEEE/ACIS International Conference on Computer and Information Science
  • Place of Presentation: ラスベガス (米国)
  • Year and Date: 2015-07-01 – 2015-07-01
  • Int'l Joint Research
• [Presentation] GRT at the SBST 2015 Tool Competition (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
  • Organizer: 8th IEEE/ACM International Workshop on Search-Based Software Testing
  • Place of Presentation: フィレンツェ (イタリア)
  • Year and Date: 2015-05-02 – 2015-05-02
  • Int'l Joint Research