Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs
Sandeep S. Kulkarni, Borzoo Bonakdarpour, and Ali Ebnenasir
Abstract
Fault-tolerance is a crucial property in many systems.
Thus, mechanical verification of algorithms associated
with synthesis of fault-tolerant programs is desirable
to ensure their correctness. In this paper, we present the
mechanized verification of algorithms that automate the
addition of fault-tolerance to a given fault-intolerant
program using the PVS theorem prover. By this verification,
not only we prove the correctness of the synthesis algorithms,
but also we guarantee that any program synthesized by these
algorithms is correct by construction. Towards this end,
we formally define a uniform framework for formal specification
and verification of fault-tolerance that consists of abstract
definitions for programs, specifications, faults, and levels of
fault-tolerance, so that they are independent of platform and
architecture. The essence of synthesis algorithms involves fixpoint
calculations. Hence, we also develop a reusable library for fixpoint
calculations on finite sets in PVS.
Paper:
Return to the publication list
Return to the Sandeep's home page