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

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

Research Project

Project/Area Number 26280019
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypePartial Multi-year Fund
Section一般
Research Field Software
Research InstitutionChiba 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 *help
¥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.

Report

(4 results)
  • 2016 Annual Research Report   Final Research Report ( PDF )
  • 2015 Annual Research Report
  • 2014 Annual Research Report
  • Research Products

    (26 results)

All 2017 2016 2015 2014

All Journal Article (15 results) (of which Int'l Joint Research: 6 results,  Peer Reviewed: 15 results,  Open Access: 13 results,  Acknowledgement Compliant: 11 results) Presentation (11 results) (of which Int'l Joint Research: 8 results)

  • [Journal Article] Model-based API Testing of Apache ZooKeeper2017

    • 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: 印刷中

    • Related Report
      2016 Annual Research Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Java Pathfinder on Android Devices2016

    • 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) Issue: 6 Pages: 1-5

    • DOI

      10.1145/3011286.3011292

    • Related Report
      2016 Annual Research Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Runtime Monitoring for Concurrent Systems2016

    • 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

    • ISBN
      9783319469812, 9783319469829
    • Related Report
      2016 Annual Research Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Precondition Coverage in Software Testing2016

    • Author(s)
      Cyrille Artho, Guillaume Rousset, Quentin Gros
    • Journal Title

      1st International Workshop on Validating Software Tests

      Volume: 印刷中

    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Classification of Randomly Generated Test Cases2016

    • Author(s)
      Cyrille Artho, Lei Ma
    • Journal Title

      1st International Workshop on Validating Software Tests

      Volume: 印刷中

    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Using Checkpointing and Virtualization for Fault Injection2015

    • 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 Issue: 2 Pages: 347-372

    • DOI

      10.15803/ijnc.5.2_347

    • NAID

      130005091738

    • ISSN
      2185-2839, 2185-2847
    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Software Model Checking of UDP-based Distributed Applications2015

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

      International Journal of Networking and Computing

      Volume: 5 Issue: 2 Pages: 373-402

    • DOI

      10.15803/ijnc.5.2_373

    • NAID

      130005091737

    • ISSN
      2185-2839, 2185-2847
    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Domain-Specific Languages with Scala2015

    • 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

    • ISBN
      9783319254227, 9783319254234
    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] GRT at the SBST 2015 Tool Competition2015

    • 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

    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] GRT: Program-Analysis-Guided Random Testing2015

    • 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

    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] GRT: An Automated Test Generator Using Orchestrated Program Analysis2015

    • 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

    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] Model-Based Testing of Stateful APIs with Modbat2015

    • 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

    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] Cardinality of UDP Transmission Outcomes2015

    • 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

    • ISBN
      9783319259413, 9783319259420
    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / 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

    • NAID

      130005091737

    • Related Report
      2014 Annual Research Report
    • 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

    • NAID

      130005091738

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed / Acknowledgement Compliant
  • [Presentation] Precondition Coverage in Software Testing2016

    • Author(s)
      Cyrille Artho
    • Organizer
      1st International Workshop on Validating Software Tests
    • Place of Presentation
      大阪大学(大阪府吹田市)
    • Year and Date
      2016-03-15
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Classification of Randomly Generated Test Cases2016

    • Author(s)
      Cyrille Artho, Lei Ma
    • Organizer
      1st International Workshop on Validating Software Tests
    • Place of Presentation
      大阪大学(大阪府吹田市)
    • Year and Date
      2016-03-15
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Domain-Specific Languages with Scala2016

    • Author(s)
      Cyrille Artho
    • Organizer
      ScalaMatsuri 2016
    • Place of Presentation
      東京国際交流館(東京都江東区)
    • Year and Date
      2016-01-31
    • Related Report
      2015 Annual Research Report
  • [Presentation] Monitoring Distributed Applications with Java Pathfinder2016

    • 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
    • Related Report
      2016 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Model-Based Testing of Stateful APIs with Modbat2015

    • 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
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] GRT: An Automated Test Generator Using Orchestrated Program Analysis2015

    • 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
    • Related Report
      2015 Annual Research Report
    • 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
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Domain-Specific Languages with Scala2015

    • 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
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Cardinality of UDP Transmission Outcomes2015

    • 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
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Using Checkpointing and Virtualization for Fault Injection2014

    • 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
    • Related Report
      2014 Annual Research Report
  • [Presentation] Systematic Analysis of Network Noise in UDP-based Applications2014

    • 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
    • Related Report
      2014 Annual Research Report

URL: 

Published: 2014-04-04   Modified: 2018-03-22  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi