Paper Abstract and Keywords |
Presentation |
2008-04-23 14:00
Generating PROMELA Models of Fault-Tolerant Distributed Algorithms Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno (Osaka Univ.) CPSY2008-5 DC2008-5 |
Abstract |
(in Japanese) |
(See Japanese page) |
(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 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) |
(in English) |
fault-tolerant distributed system / consensus problem / model checking / Heard-Of model / / / / |
Reference Info. |
IEICE Tech. Rep., vol. 108, no. 15, DC2008-5, pp. 25-30, April 2008. |
Paper # |
DC2008-5 |
Date of Issue |
2008-04-16 (CPSY, DC) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
Copyright and reproduction |
All rights are reserved and no part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission in writing from the publisher. Notwithstanding, instructors are permitted to photocopy isolated articles for noncommercial classroom use without fee. (License No.: 10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
Download PDF |
CPSY2008-5 DC2008-5 |
Conference Information |
Committee |
DC CPSY |
Conference Date |
2008-04-23 - 2008-04-23 |
Place (in Japanese) |
(See Japanese page) |
Place (in English) |
Tokyo Univ. |
Topics (in Japanese) |
(See Japanese page) |
Topics (in English) |
Dependable Computing Systems, etc. |
Paper Information |
Registration To |
DC |
Conference Code |
2008-04-DC-CPSY |
Language |
Japanese |
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 |
Keyword(5) |
|
Keyword(6) |
|
Keyword(7) |
|
Keyword(8) |
|
1st Author's Name |
Takahiro Minamikawa |
1st Author's Affiliation |
Osaka University (Osaka Univ.) |
2nd Author's Name |
Tatsuhiro Tsuchiya |
2nd Author's Affiliation |
Osaka University (Osaka Univ.) |
3rd Author's Name |
Tohru Kikuno |
3rd Author's Affiliation |
Osaka University (Osaka Univ.) |
4th Author's Name |
|
4th Author's Affiliation |
() |
5th Author's Name |
|
5th Author's Affiliation |
() |
6th Author's Name |
|
6th Author's Affiliation |
() |
7th Author's Name |
|
7th Author's Affiliation |
() |
8th Author's Name |
|
8th Author's Affiliation |
() |
9th Author's Name |
|
9th Author's Affiliation |
() |
10th Author's Name |
|
10th Author's Affiliation |
() |
11th Author's Name |
|
11th Author's Affiliation |
() |
12th Author's Name |
|
12th Author's Affiliation |
() |
13th Author's Name |
|
13th Author's Affiliation |
() |
14th Author's Name |
|
14th Author's Affiliation |
() |
15th Author's Name |
|
15th Author's Affiliation |
() |
16th Author's Name |
|
16th Author's Affiliation |
() |
17th Author's Name |
|
17th Author's Affiliation |
() |
18th Author's Name |
|
18th Author's Affiliation |
() |
19th Author's Name |
|
19th Author's Affiliation |
() |
20th Author's Name |
|
20th Author's Affiliation |
() |
Speaker |
Author-1 |
Date Time |
2008-04-23 14:00:00 |
Presentation Time |
30 minutes |
Registration for |
DC |
Paper # |
CPSY2008-5, DC2008-5 |
Volume (vol) |
vol.108 |
Number (no) |
no.14(CPSY), no.15(DC) |
Page |
pp.25-30 |
#Pages |
6 |
Date of Issue |
2008-04-16 (CPSY, DC) |
|