SMT-Based Synthesis of Fault-Tolerant Architectures

Safety-critical systems must satisfy safety requirements ensuring that catastrophic consequences of combined component failures are kept below a certain probability occurrence threshold. Therefore, designers must define a hardened architecture of the system, which fulfils the required safety level by integrating safety mechanisms. We propose an automatic SMT-based synthesis methodology to harden an initial architecture for a given safety objective. The proposed ideas are experimented on an avionics flight controller case-study and several benchmarks.