Describing and verifying malicious fault-tolerant consensus algorithms using PlusCAL and C languages
Aoi Ono, Tatsuhiro Tsuchiya · 2024
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.