Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems

Nicolas Braud-Santoni, Roderick Bloem, Swen Jacobs

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandBegutachtung

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
TitelComputer Aided Verification - 28th International Conference, CAV 2016, Proceedings
Herausgeber (Verlag)Springer-Verlag Italia
Seiten157-176
Seitenumfang20
Band9779
ISBN (Print)9783319415277
DOIs
PublikationsstatusVeröffentlicht - 2016
Veranstaltung28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, Kanada
Dauer: 17 Jul 201623 Jul 2016

Publikationsreihe

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band9779
ISSN (Print)03029743
ISSN (elektronisch)16113349

Konferenz

Konferenz28th International Conference on Computer Aided Verification, CAV 2016
Land/GebietKanada
OrtToronto
Zeitraum17/07/1623/07/16

ASJC Scopus subject areas

  • Informatik (insg.)
  • Theoretische Informatik

Fields of Expertise

  • Information, Communication & Computing

Fingerprint

Untersuchen Sie die Forschungsthemen von „Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren