Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems

Nicolas Braud-Santoni, Roderick Bloem, Swen Jacobs

Publikation: KonferenzbeitragPaperForschungBegutachtung

Abstract

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.
Originalspracheenglisch
PublikationsstatusVeröffentlicht - 17 Jun 2016

Fingerprint

Parallel algorithms
Stabilization
Temporal logic
Specifications
Formal specification

Schlagwörter

    Fields of Expertise

    • Information, Communication & Computing

    Dies zitieren

    Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems. / Braud-Santoni, Nicolas; Bloem, Roderick; Jacobs, Swen.

    2016.

    Publikation: KonferenzbeitragPaperForschungBegutachtung

    @conference{e8e37ec0b44840f98e7c060fef2e607a,
    title = "Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems",
    abstract = "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 thebounded synthesis problem with Byzantine failures more efficiently, we design anincremental, 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.",
    keywords = "Synthesis, fault tolerance, formal methods",
    author = "Nicolas Braud-Santoni and Roderick Bloem and Swen Jacobs",
    year = "2016",
    month = "6",
    day = "17",
    language = "English",

    }

    TY - CONF

    T1 - Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems

    AU - Braud-Santoni, Nicolas

    AU - Bloem, Roderick

    AU - Jacobs, Swen

    PY - 2016/6/17

    Y1 - 2016/6/17

    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 thebounded synthesis problem with Byzantine failures more efficiently, we design anincremental, 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 thebounded synthesis problem with Byzantine failures more efficiently, we design anincremental, 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

    M3 - Paper

    ER -