Hauptmenü
  • Autor
    • Braud-Santoni, Nicolas
    • Bloem, Roderick
    • Jacobs, Swen
  • TitelSynthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems
  • Volltext
  • LicenceCC-BY
  • ZugriffsrechteCC-BY
  • Download Statistik209
  • Peer ReviewJa
  • AbstractFault-tolerant distributed algorithms play an increasingly <br/>important role in many applications, and their correct and efficient <br/>implementation is notoriously difficult. We present an automatic approach <br/>to synthesise provably correct fault-tolerant distributed algorithms from <br/>formal specifications in linear-time temporal logic. The supported system <br/>model covers synchronous reactive systems with finite local state, while <br/>the failure model includes strong self-stabilisation as well as Byzantine <br/>failures. The synthesis approach for a fixed-size network of processes is <br/>complete for realisable specifications, and can optimise the <br/>solution for small implementations and short stabilisation time. To solve the<br/>bounded synthesis problem with Byzantine failures more efficiently, we design an<br/>incremental, CEGIS-like loop. Finally, we define two classes of problems <br/>for which our synthesis algorithm obtains solutions that are not only correct <br/>in fixed-size networks, but in networks of arbitrary size. <br/>