| Presentation | 2009-10-20 Model Checking-Based Agreement Verification of Consensus Algorithms Tatsuya NOGUCHI, Tatsuhiro TSUCHIYA, Tohru KIKUNO, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | This paper proposes a formal verification approach that can be applied to a class of distributed fault-tolerant protocols, namely, asynchronous consensus protocols. The proposed approach can be used to verify these protocols against agreement, the key safety property of this class of protocols. An asynchronous consensus protocol executes unbounded asynchronous rounds, and thus has a huge, often infinitely large state space. Because of this property, model checking, a widely used verification method using state exploration, is not directly applicable. In our approach, model checking is only applied to a single round of a protocol at a time, and thus the state explosion problem can be circumvented. As case studies, we verify two consensus protocols using this approach. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | consensus protocols / fault-tolerant distributed system / model checking |
| Paper # | DC2009-26 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2009/10/13(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Dependable Computing (DC) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Model Checking-Based Agreement Verification of Consensus Algorithms |
| Sub Title (in English) | |
| Keyword(1) | consensus protocols |
| Keyword(2) | fault-tolerant distributed system |
| Keyword(3) | model checking |
| 1st Author's Name | Tatsuya NOGUCHI |
| 1st Author's Affiliation | Graduate School of Information Science and Technology, Osaka University() |
| 2nd Author's Name | Tatsuhiro TSUCHIYA |
| 2nd Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| 3rd Author's Name | Tohru KIKUNO |
| 3rd Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| Date | 2009-10-20 |
| Paper # | DC2009-26 |
| Volume (vol) | vol.109 |
| Number (no) | 238 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |