Symbolic synthesis of masking fault-tolerant distributed programs

DOI10.1007/s00446-011-0139-3zbMath1285.68016OpenAlexW1983791345MaRDI QIDQ1938357

Fuad Abujarad, Sandeep S. Kulkarni, Borzoo Bonakdarpour

Publication date: 4 February 2013

Published in: Distributed Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00446-011-0139-3

zbMATH Keywords

formal methodsprogram transformationfault-tolerancedistributed programsprogram synthesissymbolic algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14) Reliability, testing and fault tolerance of networks and computer systems (68M15) Distributed algorithms (68W15)

Related Items

Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ Synthesizing bounded-time 2-phase fault recovery ⋮ Automation of fault-tolerant graceful degradation ⋮ Program repair without regret ⋮ Unnamed Item ⋮ The complexity of automated addition of fault-tolerance without explicit legitimate states

Uses Software

• NuSMV
• Sycraft

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automating the addition of fault tolerance with discrete controller synthesis
• Defining liveness
• Symbolic model checking: \(10^{20}\) states and beyond
• Symbolic model checking for real-time systems
• Synthesis of discrete-event controllers based on the signal environment
• NuSMV: A new symbolic model checker
• Undecidable problems of decentralized observation and control on regular languages
• Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• The Byzantine Generals Problem
• Think globally, act locally: decentralized supervisory control
• On the synthesis of strategies in infinite games
• On the synthesis of discrete controllers for timed systems
• Optimal Supervisory Control of Discrete Event Dynamical Systems
• Decentralized control and coordination of discrete-event systems with partial observation
• Fault Diagnosis for Timed Automata
• Correct Hardware Design and Verification Methods
• Foundations of Software Science and Computational Structures
• CONCUR 2005 – Concurrency Theory
• Computer Aided Verification