TY - GEN
T1 - Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems
AU - Braud-Santoni, Nicolas
AU - Bloem, Roderick
AU - Jacobs, Swen
PY - 2016/7/13
Y1 - 2016/7/13
N2 - Fault-tolerant distributed algorithms play an increasingly important role in many applications, and their correct and efficient implementation is notoriously difficult. We present an automatic approach to synthesise provably correct fault-tolerant distributed algorithms from formal specifications in linear-time temporal logic. The supported system model covers synchronous reactive systems with finite local state, while the failure model includes strong self-stabilisation as well as Byzantine failures. The synthesis approach for a fixed-size network of processes is complete for realisable specifications, and can optimise the solution for small implementations and short stabilisation time. To solve the bounded synthesis problem with Byzantine failures more efficiently, we design an incremental, CEGIS-like loop. Finally, we define two classes of problems for which our synthesis algorithm obtains solutions that are not only correct in fixed-size networks, but in networks of arbitrary size.
AB - Fault-tolerant distributed algorithms play an increasingly important role in many applications, and their correct and efficient implementation is notoriously difficult. We present an automatic approach to synthesise provably correct fault-tolerant distributed algorithms from formal specifications in linear-time temporal logic. The supported system model covers synchronous reactive systems with finite local state, while the failure model includes strong self-stabilisation as well as Byzantine failures. The synthesis approach for a fixed-size network of processes is complete for realisable specifications, and can optimise the solution for small implementations and short stabilisation time. To solve the bounded synthesis problem with Byzantine failures more efficiently, we design an incremental, CEGIS-like loop. Finally, we define two classes of problems for which our synthesis algorithm obtains solutions that are not only correct in fixed-size networks, but in networks of arbitrary size.
KW - Synthesis
KW - fault tolerance
KW - formal methods
UR - http://www.scopus.com/inward/record.url?scp=84978792128&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-41528-4_9
DO - 10.1007/978-3-319-41528-4_9
M3 - Conference paper
AN - SCOPUS:84978792128
SN - 9783319415277
VL - 9779
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 157
EP - 176
BT - Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings
PB - Springer-Verlag Italia
T2 - 28th International Conference on Computer Aided Verification, CAV 2016
Y2 - 17 July 2016 through 23 July 2016
ER -