Towards
Automated Model Revision for Fault-Tolerant Systems
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 are difficult to use, 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 make the automated model revision techniques easier to
use 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.
Paper:
Return to the publication list
Return to the Sandeep's home page