Automated Addition of Fault-Tolerance under Synchronous Semantics

We focus on the problem of automated model repair for synchronous systems. Model repair focuses on revising a model, so that it satisfies a new property while preserving its existing properties. While the problem of model repair has been studied previously in the context of interleaving semantics, we argue that the corresponding solutions are not applicable for several problems encountered in embedded systems. Specifically, in interleaving semantics, only one of the components executes in a given step. On the contrary, in many commonly considered distributed embedded systems, several components can execute synchronously. We present a polynomial-time sound and complete algorithm for repairing models in synchronous semantics (also called maximum parallelism semantics). We show that our approach allows us to design fault-tolerant systems, where after the occurrence of faults, the system recovers to its normal behavior within a given number of steps. We illustrate our approach by synthesizing a fault-tolerant group membership protocol and a protocol for cache coherence.