Describing and verifying malicious fault-tolerant consensus algorithms using PlusCAL and C languages
Designing distributed algorithms is challenging owing to asynchrony and faults. In this study, we formally describe two malicious fault-tolerant consensus algorithms using two languages, PlusCAL and C, and perform model checking on them. We report the observations obtained through this attempt.
Authors
- Tatsuhiro Tsuchiya (ORCID: https://orcid.org/0000-0002-3329-9235)
- Akira Ono (ORCID: https://orcid.org/0000-0001-7841-851X)
Institutions
- The University of Osaka (JP)
Publication Details
- Published
- 2024-11-13
- DOI
- https://doi.org/10.1109/prdc63035.2024.00035
- Citations
- 2
- Primary Topic
- Distributed systems and fault tolerance
- Type
- article
- Field-Weighted Citation Impact
- 0.70