| Automated model revision of distributed programs is one of the emerging and important approaches for achieving and maintaining program correctness. In this approach, an existing model is automatically revised to satisfy new properties. Such model revision is required when an existing model/program is subject to a newly identified fault, a new requirement, or a new environment. Thus, model revision is especially beneficial in the development of systems that need high assurance. To apply model revision in practice, we need to develop tools that are user friendly, comprehensive, and efficient.;However, due to their limitations, the current model revision tools and techniques are not widely used in the development of practical systems. More specifically, some of the limitation are that they suffer from a high learning curve, they require high time and space complexity, they need many details to be specified that otherwise could be automatically discovered, and they do not cover different types of revision.;Taking into consideration the aforementioned limitations, in this dissertation, we derive theories, develop algorithms, and build tools to advance the state-of-the-art of the automated model revision. Our approach comprises four main elements: First, we reduce the learning curve for the automated model revision techniques by utilizing existing design tools to perform the revision under-the-hood. Second, to permit the designer to efficiently describe the model to be synthesized and to minimize the user input, we develop algorithms and tools to automate the generation of the legitimate states of the original model, thereby reducing the burden of the designer. Third, to utilize the available computing resources and to efficiently complete the revision, we utilize both symmetry and parallelism to speedup the automated revision and to overcome its bottlenecks. Fourth, to provide comprehensive revision and to cover more types of model revision, such as nonmasking and stabilizing fault-tolerance, we develop algorithms and tools to allow for addition of new types of fault- tolerance. To validate our approach and illustrate its feasibility, we apply it to several case studies. |
