Search results

Title: Automated revision of distributed and real-time programs
Creator: Bonakdarpour, Borzoo
Date: 2009
Collection: Electronic Theses & Dissertations

Title: Automatic verification and revision of multitolerant programs
Creator: Chen, Jingshu
Date: 2013
Collection: Electronic Theses & Dissertations
Description: 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...
Show moreThe 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.
Show less

Title: Using evolutionary approach to optimize and model multi-scenario, multi-objective fault-tolerant problems
Creator: Zhu, Ling (Engineer)
Date: 2017
Collection: Electronic Theses & Dissertations
Description: Fault-tolerant design involves different scenarios, such as scenarios with no fault in the system, with faults occurring randomly, with different operation conditions, and with different loading conditions. For each scenario, there can be multiple requirements (objectives). To assess the performance of a design (solution), it needs to be evaluated over a number of different scenarios containing various requirements in each scenario. We consider this problem as a multi-scenario, multi...
Show moreFault-tolerant design involves different scenarios, such as scenarios with no fault in the system, with faults occurring randomly, with different operation conditions, and with different loading conditions. For each scenario, there can be multiple requirements (objectives). To assess the performance of a design (solution), it needs to be evaluated over a number of different scenarios containing various requirements in each scenario. We consider this problem as a multi-scenario, multi-objective (MSMO) problem.Despite its practical importance and prevalence in engineering application, there are not many studies which systematically solve the MSMO problem. In this dissertation, we focus on optimizing and modeling MSMO problems, and propose various approaches to solve different types of MSMO optimization problems, especially multi-objective fault-tolerant problems. We classify MSMO optimization problem into two categories: scenario-dependent and scenario-independent. For the scenario-dependent MSMO problem, we review existing methodologies and suggest two evolutionary-based methods for handling multiple scenarios and objectives: aggregated method and integrated method. The effectiveness of both methods are demonstrated on several case studies including numerical problems and engineering design problems. The engineering problems include cantilever-type welded beam design, truss bridge design, four-bar truss design. The experimental results show that both methods can find a set of widely distributed solutions that are compromised among the respective objective values under all scenarios. We also model fault-tolerant programs using the aggregated method. We synthesize three fault-tolerant distributed programs: Byzantine agreement program, token ring circulation program and consensus program with failure detector $S$. The results show that evolutionary-base MSMO approach, as a generic method, can effectively model fault-tolerant programs. For the scenario-independent MSMO problem, we apply evolutionary multi-objective approach. As a case study, we optimize a probabilistic self-stabilizing program, a special type of fault-tolerant program, and obtain several interesting counter-intuitive observations under different scenarios.
Show less