実行時検証とモデル検査の融合によるネットワークソフトウェアの統合実行監視

2015 Fiscal Year Annual Research Report

• Project/Area Number: 26280019
• Research Institution: Chiba University
• Principal Investigator: 山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
• Co-Investigator(Kenkyū-buntansha): 萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252) ; Artho Cyrille 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (30462831) ; 山形 頼之 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415758) ; 田辺 良則 鶴見大学, 文学部, 教授 (60443199)
• Project Period (FY): 2014-04-01 – 2017-03-31
• Keywords: 実環境モデル検査 / 実行時検証 / ネットワークソフトウェア

Outline of Annual Research Achievements

研究期間全体を通して、以下の3つの部品それぞれに対応するサブプロジェクトに分割して研究を進めている。(1) net-iocache: ネットワーク環境において検査対象を管理するためのJava Pathfinder(JPF)拡張。(2) net-monitor: JPF内外のネットワークプロセスからイベントを収集し、実行監視による実行時検査を行う部分。最終的にはnet-iocacheと統合される。(3) peer-monitor: 通信相手のプロセスからnet-monitorにイベントを送るツール。
(1)については、我々が先行研究課題でネットワークアプリケーションのモデル検査のために開発したnet-iocacheを、イベント取得や他コンポーネントとの連携、より柔軟なバックトラッキングに対応できるように再設計・再実装した。以前のバージョンに比肩する性能を保ちながら、長時間稼動させても安定して動作する堅牢性を兼ね備えていることを実験により確認した。net-iocacheの実装部分については今年度で完成と考えている。これらの成果はnet-iocache v2として論文にまとめ、発表することを予定している。(2)については、前年度に基本設計を行った実行監視部分とモデル検査器部分との連携部分について、プロトタイプ実装を進めている。(3)については前年度に引き続いて、実行監視のための論理/形式体系として、CSPを拡張した言語の検査器CSP_EをScala上に実装し、効率の改良および実例を用いた既存体系との比較、形式的意味論の構築を行っている。
研究協力者 馬雷 (千葉大学) ヴァイテル・フランツ (千葉大学)

Current Status of Research Progress

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

Reason

研究実績の概要で述べた3項目(1)(2)(3)ともに、年度当初に予定していた計画をほぼ順調に達成している。特に(1)については、先行研究課題からの継続という側面が強いこともあり、実装面について当初の予定通り平成27年度中に完了している。

Strategy for Future Research Activity

最終年度に向けて、特に以下の2点に注力して推進する。(1)準備中あるいはまだ国際会議等に採択されていない論文を仕上げ、採択を目指す。(2)最終成果物として動作するよう、各サブプロジェクトの内容をまとめ上げる。

Causes of Carryover

当初計画では平成26年度後半からと考えていたポスドク研究者の雇用が、実際には平成26年度11月中旬からとなったため。
また、初年度に採択された論文の国際会議が国内で開催されたものであったため。

Expenditure Plan for Carryover Budget

平成28年度分として請求した助成金と併せ、主に平成28年度のポスドク研究者雇用費として、また国際会議に投稿を準備している論文の発表のための旅費として使用する。

Research Products

• [Journal Article] Precondition Coverage in Software Testing (2016)
  • Author(s): Cyrille Artho, Guillaume Rousset, Quentin Gros
  • Journal Title: 1st International Workshop on Validating Software Tests Volume: 印刷中 Pages: 印刷中
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Classification of Randomly Generated Test Cases (2016)
  • Author(s): Cyrille Artho, Lei Ma
  • Journal Title: 1st International Workshop on Validating Software Tests Volume: 印刷中 Pages: 印刷中
  • Peer Reviewed / Open Access
• [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: Vol. 5, No. 2 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: Vol. 5, No. 2 Pages: 373～402
  • DOI: 10.15803/ijnc.5.2_373
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Domain-Specific Languages with Scala (2015)
  • Author(s): Cyrille Artho, Klaus Havelund, Rahul Kumar, Yoriyuki Yamagata
  • Journal Title: Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015 Volume: LNCS 9407 Pages: 1～16
  • DOI: 10.1007/978-3-319-25423-4_1
  • Peer Reviewed / Open Access / Int'l Joint Research
• [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: IEEE/ACM 8th International Workshop on Search-Based Software Testing Volume: 該当なし Pages: 48～51
  • DOI: 10.1109/SBST.2015.19
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] GRT: Program-Analysis-Guided Random Testing (T) (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Journal Title: 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 該当なし Pages: 212～223
  • DOI: 10.1109/ASE.2015.49
  • Peer Reviewed / Open Access / 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: 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 該当なし Pages: 842～847
  • DOI: 10.1109/ASE.2015.102
  • Peer Reviewed / Open Access / Int'l Joint Research / 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: 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 該当なし Pages: 858～863
  • DOI: DOI 10.1109/ASE.2015.95
  • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [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: Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015 Volume: LNCS 9409 Pages: 120～134
  • DOI: 10.1007/978-3-319-25942-0_8
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Presentation] Precondition Coverage in Software Testing (2016)
  • Author(s): Cyrille Artho
  • 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 (2016)
  • Author(s): Cyrille Artho
  • Organizer: ScalaMatsuri 2016
  • Place of Presentation: 東京国際交流館(東京都江東区)
  • Year and Date: 2016-01-31 – 2016-01-31
• [Presentation] Model-Based Testing of Stateful APIs with Modbat (2015)
  • Author(s): Cyrille Artho
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: Lincoln (USA)
  • 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
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: Lincoln (USA)
  • Year and Date: 2015-11-12 – 2015-11-12
  • Int'l Joint Research
• [Presentation] GRT: Program-Analysis-Guided Random Testing (T) (2015)
  • Author(s): Lei Ma
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: Lincoln (USA)
  • Year and Date: 2015-11-11 – 2015-11-11
  • Int'l Joint Research
• [Presentation] Domain-Specific Languages with Scala (2015)
  • Author(s): Cyrille Artho
  • Organizer: 17th International Conference on Formal Engineering Methods, ICFEM 2015
  • Place of Presentation: Paris (France)
  • Year and Date: 2015-11-05 – 2015-11-05
  • Int'l Joint Research
• [Presentation] Cardinality of UDP Transmission Outcomes (2015)
  • Author(s): Franz Weitl
  • Organizer: Symposium on Dependable Software Engineering: Theories, Tools and Applications
  • Place of Presentation: Nanjing (China)
  • Year and Date: 2015-11-04 – 2015-11-04
  • Int'l Joint Research