| Presentation | 2005/6/10 Model Checking a Distributed Consensus Algorithm against a Safety Property Takafumi MATSUO, Tatsuhiro TSUCHIYA, Tohru KIKUNO, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | The consensus problem is one of the most important problems in the field of distributed computing. In this paper, we discuss the applicability of model checking to verification of consensus algorithms. Model checking is a technique for determining whether or not a given property holds by exploring a finite state space that models the behavior of a system. We verify a safety property of Chandra-Toueg algorithm, a well-known consensus algorithm, by using a model checking tool SPIN. We devise several techniques for reducing the state space. In this paper, we show these techniques as well as the result of verification. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | distributed system / consensus problem / model checking / Chandra-Toueg algorithm |
| Paper # | DC2005-7 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2005/6/10(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 a Distributed Consensus Algorithm against a Safety Property |
| Sub Title (in English) | |
| Keyword(1) | distributed system |
| Keyword(2) | consensus problem |
| Keyword(3) | model checking |
| Keyword(4) | Chandra-Toueg algorithm |
| 1st Author's Name | Takafumi MATSUO |
| 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 | 2005/6/10 |
| Paper # | DC2005-7 |
| Volume (vol) | vol.105 |
| Number (no) | 123 |
| Page | pp.pp.- |
| #Pages | 5 |
| Date of Issue | |