Model Checking Network Applications using Distributed Checkpointing

• Project/Area Number: 23300004
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Chiba University
• Principal Investigator: YAMAMOTO Mitsuharu 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
• Co-Investigator(Kenkyū-buntansha): HAGIYA Masami 東京大学, 情報理工学系研究科, 教授 (30156252) ; ARTHO Cyrille 独立行政法人産業技術総合研究所, セキュアシステム研究部門, 主任研究員 (30462831) ; TANABE Yoshinori 国立情報学研究所, アーキテクチャ科学系, 特任教授 (60443199)
• Research Collaborator: LEUNGWATTANAKIT Watcharin 東京大学 ; WEITL Franz 千葉大学 ; POTTER Richard 東京大学 ; SEBIH Nazim 東京大学
• Project Period (FY): 2011-04-01 – 2014-03-31
• Project Status: Completed (Fiscal Year 2013)
• Budget Amount: ¥19,240,000 (Direct Cost: ¥14,800,000、Indirect Cost: ¥4,440,000); Fiscal Year 2013: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2012: ¥10,140,000 (Direct Cost: ¥7,800,000、Indirect Cost: ¥2,340,000); Fiscal Year 2011: ¥5,720,000 (Direct Cost: ¥4,400,000、Indirect Cost: ¥1,320,000)
• Keywords: モデル検査 / チェックポインティング

Research Abstract

With distributed checkpointing, we enhanced our previous results on model checking network applications so that it can check network applications on more complicated and practical environments. This was accomplished by implementing communication resumption on distributed checkpointing. We also adopted newer network API that is used in practical network applications so as to check wider range of applications.

Research Products

• [Journal Article] Modular Software Model Checking for Distributed Systems (2014)
  • Author(s): Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, and Koichi Takahashi
  • Journal Title: IEEE Transactions on Software Engineering Volume: - Issue: 5 Pages: 483-501
  • DOI: 10.1109/tse.2013.49
  • Peer Reviewed
• [Journal Article] Modbat: A Model-Based API Tester for Event-Driven Systems (2013)
  • Author(s): Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, and Mitsuharu Yamamoto
  • Journal Title: Proceedings of the 9th Haifa Verification Conference, Lecture Notes in Computer Science Volume: 8244 Pages: 112-128
  • DOI: 10.1007/978-3-319-03077-7_8
  • ISBN: 9783319030760, 9783319030777
  • Peer Reviewed
• [Journal Article] Software Model Checking for Distributed Systems with Selector-Based, Non-blocking Communication (2013)
  • Author(s): Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, and Mitsuharu Yamamoto
  • Journal Title: 28th IEEE/ACM International Conference on Automated Software Engineering Volume: - Pages: 169-179
  • DOI: 10.1109/ase.2013.6693077
  • Peer Reviewed
• [Journal Article] Model checking distributed systems by combining caching and process checkpointing (2011)
  • Author(s): Watcharin Leungwattanakit
  • Journal Title: 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) Volume: 1 Pages: 103-112
  • DOI: 10.1109/ase.2011.6100043
  • Peer Reviewed
• [Presentation] Modbat : A model-based API tester for event-driven systems (2012)
  • Author(s): Cyrille Artho
  • Organizer: 第10回ディペンダブルシステムワークショップ(DSW2012)
  • Place of Presentation: 独立行政法人理化学研究所計算科学研究機構
• [Presentation] Modbat: A model-based API tester for event-driven systems (2012)
  • Author(s): Cyrille Artho
  • Organizer: 第10回 ディペンダブルシステムワークショップ (DSW 2012)
  • Place of Presentation: 独立行政法人理化学研究所 計算科学研究機構
• [Remarks]
  • URL: http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache
• [Remarks] projects/net-iocache - Java Path Finder
  • URL: http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache
• [Remarks]
  • URL: http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/net-iocache