Model Checking of Fault-Tolerant Algorithms for the Dependability of Distributed Systems

• Project/Area Number: 20700026
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: Osaka University
• Principal Investigator: TSUCHIYA Tatsuhiro Osaka University, 大学院・情報科学研究科, 准教授 (30283740)
• Project Period (FY): 2008 – 2010
• Project Status: Completed (Fiscal Year 2010)
• Budget Amount: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2010: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2009: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2008: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
• Keywords: 仕様記述 / 仕様検証 / 分散アルゴリズム / モデル検査

Research Abstract

A mechanical verification approach is proposed to verify consensus algorithms, which are core algorithms that can be used in implementing fault-tolerant distributed systems. Experiment results show that when an abstract distributed system model is assumed, our approach can scale up to around ten computing nodes.

Research Products

• [Journal Article] Andre Schiper, Verification of Consensus Algorithms Using Satisfiability Solving (2011)
  • Author(s): Tatsuhiro Tsuchiya
  • Journal Title: Distributed Computing 23 Pages: 341-358
  • Peer Reviewed
• [Journal Article] Verification of Consensus Algorithms Using Satisfiability Solving (2011)
  • Author(s): Tatsuhiro Tsuchiya, Andre Schiper
  • Journal Title: Distributed Computing Volume: (印刷中)
  • Peer Reviewed
• [Journal Article] Towards Automated Verification of Distributed Consensus Protocols (2009)
  • Author(s): Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno
  • Journal Title: Proceedings of 16th Asia-Pacific Software Engineering Conference (APSEC 2009) Pages: 499-506
  • Peer Reviewed
• [Journal Article] Towards Automated Verification of Distributed Consensus Protocols (2009)
  • Author(s): Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno
  • Journal Title: Proceedings of 16th Asia-Pacific Software Enginee ring Conference (APSEC 2009) Pages: 499-506
  • Peer Reviewed
• [Journal Article] Tohru Kikuno, Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms (2008)
  • Author(s): Takahiro Minamikawa, Tatsuhiro Tsuchiya
  • Journal Title: Proceedings of 11th International Symposium on Pacific Rim Dependable Computing Pages: 40-47
  • Peer Reviewed
• [Journal Article] Andre Schiper, Using Bounded Model Checking to Verify Consensus Algorithms (2008)
  • Author(s): Tatsuhiro Tsuchiya
  • Journal Title: Lecture Note on Computer Science 5218 Pages: 466-480
  • Peer Reviewed
• [Journal Article] Using Bounded Model Checking to Verify Consensus Algorithms (2008)
  • Author(s): Tatsuhiro Tsuchiya, Andre Schiper
  • Journal Title: Lecture Note on Computer Science 5218 Pages: 466-480
  • Peer Reviewed
• [Journal Article] Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms (2008)
  • Author(s): Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno
  • Journal Title: Proceedings of 11th International Symposium on Pacific Rim Dependable Computing Pages: 40-47
  • Peer Reviewed
• [Presentation] Model Checking of Unbounded Rounds of Asynchronous Consensus Protocols (2010)
  • Author(s): Tatsuhiro Tsuchiya, Andre chiper
  • Organizer: Workshop on Dependability of Network Software Applications 2010
  • Place of Presentation: 広島大学(広島県)
  • Year and Date: 2010-11-18
• [Presentation] Safety Verification of Asynchronous Consensus Algorithms Using Model Checking (2009)
  • Author(s): Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno
  • Organizer: 2nd International Workshop on Reliability, Availability, and Security (WRAS)
  • Place of Presentation: 広島大学(広島県)
  • Year and Date: 2009-12-11
• [Presentation] Safety Verification of Asynchronous Consensus Algorithms Using Model Checking (2009)
  • Author(s): Tatsuya Noguchi, Tatsuhiro Tsuchiya, Tohru Kikuno
  • Organizer: 2nd International Workshop on Reliability, Availability, and Security (WRAS)
  • Place of Presentation: 広島大学 (広島県)
  • Year and Date: 2009-12-11
• [Presentation] モデル検査を用いたコンセンサスアルゴリズムの合意性検証 (2009)
  • Author(s): 野口達也, 土屋達弘, 菊野亨
  • Organizer: 電子情報通信学会ディペンダブルコンピューティング研究会
  • Place of Presentation: 機械振興会館(東京)
  • Year and Date: 2009-10-13
• [Presentation] 耐故障分散アルゴリズムに対するPROMELAモデルの生成 (2008)
  • Author(s): 南川恭洋, 土屋達弘, 菊野亨
  • Organizer: 電子情報通信学会ディペンダブルコンピューティング研究会
  • Place of Presentation: 東京
  • Year and Date: 2008-04-23