ディペンダブル分散システム実現のための耐故障アルゴリズムのモデル検査

• 研究課題/領域番号: 20700026
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 大阪大学
• 研究代表者: 土屋 達弘 大阪大学, 大学院・情報科学研究科, 准教授 (30283740)
• 研究期間 (年度): 2008 – 2010
• 研究課題ステータス: 完了 (2010年度)
• 配分額: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円); 2010年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2009年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2008年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
• キーワード: 仕様記述 / 仕様検証 / 分散アルゴリズム / モデル検査

研究概要

コンセンサスアルゴリズムと呼ばれる,複数の計算機から構成される分散システム上で耐故障性を実現するためのアルゴリズムに対し,その正しさを自動的に検証する手法を開発した.抽象度の高いシステムモデルを仮定した場合,対象システムが計算機10台程度の規模であれば,プログラムを用いて機械的に検証が可能ことを実験的に示した.

研究成果

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