| Presentation | 2008-04-23 Generating PROMELA Models of Fault-Tolerant Distributed Algorithms Takahiro MINAMIKAWA, Tatsuhiro TSUCHIYA, Tohru KIKUNO, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | The consensus problem is fundamental in implementing fault-tolerant distributed systems. However, designing a correct consensus algorithm is difficult. Therefore a verification method for consensus algorithms is necessary. The purpose of this study is to facilitate the verification of Heard-Of model-based consensus algorithms with the SPIN model checker. To this end, we propose a transformation method that generates an input model to SPIN from a given consensus algorithm and an algorithm description language. The Heard-Of model is a computation model which allows one to formally treat fault-prone asynchronous systems. We also show the results of verifying several consensus algorithms with the transformation method to show its usefulness. A notable finding of the case studies was that a design fault was successfully detected in an erroneous algorithm. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | fault-tolerant distributed system / consensus problem / model checking / Heard-Of model |
| Paper # | CPSY2008-5,DC2008-5 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2008/4/16(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) | Generating PROMELA Models of Fault-Tolerant Distributed Algorithms |
| Sub Title (in English) | |
| Keyword(1) | fault-tolerant distributed system |
| Keyword(2) | consensus problem |
| Keyword(3) | model checking |
| Keyword(4) | Heard-Of model |
| 1st Author's Name | Takahiro MINAMIKAWA |
| 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 | 2008-04-23 |
| Paper # | CPSY2008-5,DC2008-5 |
| Volume (vol) | vol.108 |
| Number (no) | 15 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |