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

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

Research Project

Project/Area Number 20700026
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Software
Research InstitutionOsaka University

Principal Investigator

TSUCHIYA Tatsuhiro  Osaka University, 大学院・情報科学研究科, 准教授 (30283740)

Project Period (FY) 2008 – 2010
Project Status Completed (Fiscal Year 2010)
Budget Amount *help
¥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.

Report

(4 results)
  • 2010 Annual Research Report   Final Research Report ( PDF )
  • 2009 Annual Research Report
  • 2008 Annual Research Report
  • Research Products

    (13 results)

All 2011 2010 2009 2008

All Journal Article (8 results) (of which Peer Reviewed: 8 results) Presentation (5 results)

  • [Journal Article] Andre Schiper, Verification of Consensus Algorithms Using Satisfiability Solving2011

    • Author(s)
      Tatsuhiro Tsuchiya
    • Journal Title

      Distributed Computing 23

      Pages: 341-358

    • Related Report
      2010 Final Research Report
    • Peer Reviewed
  • [Journal Article] Verification of Consensus Algorithms Using Satisfiability Solving2011

    • Author(s)
      Tatsuhiro Tsuchiya, Andre Schiper
    • Journal Title

      Distributed Computing

      Volume: (印刷中)

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Towards Automated Verification of Distributed Consensus Protocols2009

    • Author(s)
      Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno
    • Journal Title

      Proceedings of 16th Asia-Pacific Software Engineering Conference (APSEC 2009)

      Pages: 499-506

    • Related Report
      2010 Final Research Report
    • Peer Reviewed
  • [Journal Article] Towards Automated Verification of Distributed Consensus Protocols2009

    • Author(s)
      Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno
    • Journal Title

      Proceedings of 16th Asia-Pacific Software Enginee ring Conference (APSEC 2009)

      Pages: 499-506

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Tohru Kikuno, Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms2008

    • Author(s)
      Takahiro Minamikawa, Tatsuhiro Tsuchiya
    • Journal Title

      Proceedings of 11th International Symposium on Pacific Rim Dependable Computing

      Pages: 40-47

    • Related Report
      2010 Final Research Report
    • Peer Reviewed
  • [Journal Article] Andre Schiper, Using Bounded Model Checking to Verify Consensus Algorithms2008

    • Author(s)
      Tatsuhiro Tsuchiya
    • Journal Title

      Lecture Note on Computer Science 5218

      Pages: 466-480

    • Related Report
      2010 Final Research Report
    • Peer Reviewed
  • [Journal Article] Using Bounded Model Checking to Verify Consensus Algorithms2008

    • Author(s)
      Tatsuhiro Tsuchiya, Andre Schiper
    • Journal Title

      Lecture Note on Computer Science 5218

      Pages: 466-480

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms2008

    • Author(s)
      Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno
    • Journal Title

      Proceedings of 11th International Symposium on Pacific Rim Dependable Computing

      Pages: 40-47

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Presentation] Model Checking of Unbounded Rounds of Asynchronous Consensus Protocols2010

    • Author(s)
      Tatsuhiro Tsuchiya, Andre chiper
    • Organizer
      Workshop on Dependability of Network Software Applications 2010
    • Place of Presentation
      広島大学(広島県)
    • Year and Date
      2010-11-18
    • Related Report
      2010 Annual Research Report 2010 Final Research Report
  • [Presentation] Safety Verification of Asynchronous Consensus Algorithms Using Model Checking2009

    • 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
    • Related Report
      2010 Final Research Report
  • [Presentation] Safety Verification of Asynchronous Consensus Algorithms Using Model Checking2009

    • 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
    • Related Report
      2009 Annual Research Report
  • [Presentation] モデル検査を用いたコンセンサスアルゴリズムの合意性検証2009

    • Author(s)
      野口達也, 土屋達弘, 菊野亨
    • Organizer
      電子情報通信学会ディペンダブルコンピューティング研究会
    • Place of Presentation
      機械振興会館(東京)
    • Year and Date
      2009-10-13
    • Related Report
      2010 Final Research Report
  • [Presentation] 耐故障分散アルゴリズムに対するPROMELAモデルの生成2008

    • Author(s)
      南川恭洋, 土屋達弘, 菊野亨
    • Organizer
      電子情報通信学会ディペンダブルコンピューティング研究会
    • Place of Presentation
      東京
    • Year and Date
      2008-04-23
    • Related Report
      2008 Annual Research Report

URL: 

Published: 2008-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi