Lazy Repair for Addition of Fault-Tolerance to Distributed Programs
Mohammad Roohitavaf, Yiyan Lin, Sandeep S. Kulkarni · 2016
We focus on the issue of realizability constraints in the context of model repair. Model repair focuses on revising a given program to satisfy new properties of interest while satisfying existing properties such as fault-tolerance. An important difficulty in using model repair is that the repaired model must be realizable in the constraints given by the underlying system. It is well-known that these realizability constraints cause an increase in the complexity of model repair (e.g., from P to NP-complete). Hence, existing approaches for adding fault-tolerance to distributed program focuses on cautious repair where in every step, the model being repaired satisfies the realizability constraints. They also utilize heuristics to reduce the complexity of repair. In this work, we focus on using lazy repair while adding fault-tolerance. Specifically, in this work, we utilize a two-step approach. The first step ignores the realizability constraints and performs model repair to add fault-tolerance. This ensures that the resulting program satisfies the desired property of interest (namely, fault-tolerance) although it may not be realizable. The second step attempts to revise this program to ensure that realizability constraints are satisfied without creating new program behaviors. This ensures that the resulting program satisfies both the properties of interest and realizability constraints. We demonstrate that this approach is more efficient than the cautious repair algorithm in the literature. We also note that inherently the lazy repair approach is also applicable in other contexts such as synchronous systems, cyber-physical systems, etc.