Automatic verification and revision of multitolerant programs

The notion of multitolerance is based on the observation that modern programs are often subject to multiple faults. And, the requirements in the presence of these faults vary based on the nature of the faults, its severity and the cost of providing fault-tolerance to it. Also, assurance of multitolerant systems is necessary via they are integral parts of our lives. This dissertation proposes to provide such assurance via automated verification and revision. Regarding verification, we focus on verification of self-stabilization, which is the ability of the program to recover from arbitrary states. We consider verification of self-stabilization because several multitolerant systems are indeed stabilizing. Also, most of literature on verification of fault-tolerance focuses on safety property; our work complements it by considering liveness properties. Hence, we envision verification of multitolerant programs by using existing approaches for verifying safety and using the results from this dissertation for verifying liveness. We propose a technique that is based on a bottleneck (fairness requirements) identified in existing work on verification of stabilization. Our approach uses the role of fairness along with symbolic model checking, and hence reduces the cost of verification substantially. We also propose a constraint-based approach that reduces the task of verifying self-stabilization into a well-studied problem of constraint solving, so that one can leverage the use of existing highly optimized solutions (SAT/SMT solvers) to reduce the verification cost. Regarding revision, we focus on revising existing programs to obtain the corresponding multitolerant ones. Revising the program manually is expensive since it requires additional verification steps to guarantee correctness. Also, manual revision may violate existing requirements. For these reasons, we propose an automatic approach to revise a given program to add multitolerance to the given class(es) of faults. Specifically, we characterize multitolerance in terms of strong multitolerance and weak multitolerance. Intuitively, strong multitolerance provides higher guarantees than weak multitolerance. However, there are scenarios where designing a strong multitolerant program is expensive or impossible although designing weak multitolerance is feasible. We investigate the complexity of automatic revision for adding multitolerance. In particular, we identify instances where adding weak multitolerance is NP-hard even though adding strong multitolerance in the same setting in P. We also develop algorithms (and heuristics) for automatic revision for adding multitolerance to existing programs. We implement these algorithms in a model repair tool for automatically adding multitolerance. Additionally, we build a lightweight framework that utilizes our model repair tool for automatically revising UML state diagram for adding fault-tolerance. This framework has several practical and methodological significance regarding the development of concurrent software. Specifically, this framework allows designers to revise an existing UML model to add fault-tolerance without a detailed knowledge of the formalism behind model repair algorithms.