caa a22 4500 445355158 CHVBK 20180317142857.0 cr unu---uuuuu 170323e20110401xx s 000 0 eng 10.1007/s00446-010-0123-3 doi (NATIONALLICENCE)springer-10.1007/s00446-010-0123-3 Verification of consensus algorithms using satisfiability solving [Elektronische Daten] [Tatsuhiro Tsuchiya, André Schiper] Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms, aiming at facilitating their development. Our approach uses model checking, a widely practiced verification method based on state traversal. The challenge here is that the state space of these algorithms is huge, often infinite, thus making model checking infeasible. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a small, finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used to solve these problems. The proposed approach allows us to model check several consensus algorithms up to around 10 processes. Springer-Verlag, 2010 Consensus nationallicence Model checking nationallicence Fault-tolerant distributed algorithms nationallicence Formal verification nationallicence Tsuchiya Tatsuhiro Osaka University, 1-5 Yamadaoka, Suita, 565-0871, Osaka, Japan aut Schiper André École Polytechnique Fédérale de Lausanne (EPFL), 1015, Lausanne, Switzerland aut Distributed Computing Springer-Verlag 23/5-6(2011-04-01), 341-358 0178-2770 23:5-6<341 2011 23 446 https://doi.org/10.1007/s00446-010-0123-3 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s00446-010-0123-3 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Tsuchiya Tatsuhiro Osaka University, 1-5 Yamadaoka, Suita, 565-0871, Osaka, Japan aut NATIONALLICENCE 700 1- Schiper André École Polytechnique Fédérale de Lausanne (EPFL), 1015, Lausanne, Switzerland aut NATIONALLICENCE 773 0- Distributed Computing Springer-Verlag 23/5-6(2011-04-01), 341-358 0178-2770 23:5-6<341 2011 23 446 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer