Integrated Runtime Monitoring of Network Software by Fusion of Runtime Verification and Model Checking

• Project/Area Number: 26280019
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Partial Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Chiba University
• Principal Investigator: Yamamoto Mitsuharu 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
• Co-Investigator(Kenkyū-buntansha): 萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252) ; Artho Cyrille (ARTHO Cyrille) 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (30462831) ; 山形 頼之 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415758) ; 田辺 良則 鶴見大学, 文学部, 教授 (60443199)
• Research Collaborator: KOHAN Alexander 千葉大学 ; WEITL Franz 千葉大学 ; MA Lei 千葉大学 ; SEBIH Nazim 東京大学
• Project Period (FY): 2014-04-01 – 2017-03-31
• Project Status: Completed (Fiscal Year 2016)
• Budget Amount: ¥17,160,000 (Direct Cost: ¥13,200,000、Indirect Cost: ¥3,960,000); Fiscal Year 2016: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000); Fiscal Year 2015: ¥7,410,000 (Direct Cost: ¥5,700,000、Indirect Cost: ¥1,710,000); Fiscal Year 2014: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000)
• Keywords: 実環境モデル検査 / 実行時検証 / ネットワークソフトウェア

Outline of Final Research Achievements

By fusing runtime verification and model checking, we proposed a framework to verify global specification of network systems with taking account of thread scheduling nondeterminism of the system under test, and implemented its prototype.
Runtime verification alone cannot deal with thread scheduling nondeterminism, and model checking alone cannot handle properties of the whole network system consisting of the system under test and remote peers. By fusing both techniques, we made it possible to detect bugs that cannot be manifested only by existing model checking against the system under test.

Research Products

• [Journal Article] Model-based API Testing of Apache ZooKeeper (2017)
  • Author(s): Cyrille Valentin Artho, Quentin Gros, Guillaume Rousset, Kazuaki Banzai, Lei Ma, Takashi Kitamura, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto
  • Journal Title: 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017) Volume: 印刷中
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Java Pathfinder on Android Devices (2016)
  • Author(s): Alexander Kohan, Mitsuharu Yamamoto, Cyrille Artho, Yoriyuki Yamagata, Lei Ma, Masami Hagiya, and Yoshinori Tanabe
  • Journal Title: ACM SIGSOFT Software Engineering Notes Volume: 41(6) Pages: 1-5
  • DOI: 10.1145/3011286.3011292
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Runtime Monitoring for Concurrent Systems (2016)
  • Author(s): Yoriyuki Yamagata, Cyrille Artho, Masami Hagiya, Jun Inoue, Lei Ma, Yoshinori Tanabe, and Mitsuharu Yamamoto
  • Journal Title: Runtime Verification - 16th International Conference, (RV 2016) Volume: LNCS 10012 Pages: 386-403
  • DOI: 10.1007/978-3-319-46982-9_24
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [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: 印刷中
  • 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: 印刷中
  • 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: IJNC Volume: 5 Issue: 2 Pages: 347-372
  • DOI: 10.15803/ijnc.5.2_347
  • NAID: 130005091738
  • ISSN: 2185-2839, 2185-2847
  • 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: IJNC Volume: Vol. 5, No. 2 Issue: 2 Pages: 373-402
  • DOI: 10.15803/ijnc.5.2_373
  • NAID: 130005091737
  • ISSN: 2185-2839, 2185-2847
  • 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: 2015 Pages: 1-16
  • DOI: 10.1007/978-3-319-25423-4_1
  • Peer Reviewed / Open Access / 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: IEEE/ACM 8th International Workshop on Search-Based Software Testing Volume: 2015 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: 2015 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: 2015 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: 2015 Pages: 858-863
  • 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: 2015 Pages: 120-134
  • DOI: 10.1007/978-3-319-25942-0_8
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Software Model Checking of UDP-based Distributed Applications (2014)
  • Author(s): Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
  • Journal Title: Second International Symposium on Computing and Networking (CANDAR), 2014 Volume: 2014 Pages: 96-105
  • DOI: 10.1109/candar.2014.66
  • NAID: 130005091737
  • Peer Reviewed
• [Journal Article] Using Checkpointing and Virtualization for Fault Injection (2014)
  • Author(s): Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
  • Journal Title: Second International Symposium on Computing and Networking (CANDAR), 2014 Volume: 2014 Pages: 144-150
  • DOI: 10.1109/candar.2014.45
  • NAID: 130005091738
  • Peer Reviewed / 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
  • 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
  • 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
• [Presentation] Monitoring Distributed Applications with Java Pathfinder (2016)
  • Author(s): Lei Ma, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Alexander Kohan and Mitsuharu Yamamoto
  • Organizer: Java Pathfinder Workshop 2016
  • Place of Presentation: Seattle, USA
  • Int'l Joint Research
• [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
  • 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
  • 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
  • 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
  • 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
  • Int'l Joint Research
• [Presentation] Using Checkpointing and Virtualization for Fault Injection (2014)
  • Author(s): Cyrille Artho
  • Organizer: CANDAR'14: The Second International Symposium on Computing and Networking - Across Practical Development and Theoretical Research -
  • Place of Presentation: 静岡県静岡市
  • Year and Date: 2014-12-11
• [Presentation] Systematic Analysis of Network Noise in UDP-based Applications (2014)
  • Author(s): Nazim Sebih
  • Organizer: CANDAR'14: The Second International Symposium on Computing and Networking - Across Practical Development and Theoretical Research -
  • Place of Presentation: 静岡県静岡市
  • Year and Date: 2014-12-10