Abstract
Executable assertions embedded into a distributed computing system can provide run-time assurance by ensuring that the program state, in the actual run-time environment, is consistent with the logical stage specified in the assertions; if not, then an error has occurred and a reliable communication of this diagnostic information is provided to the system such that reconfiguration and recovery can take place. Application- oriented fault tolerance is a method that provides fault detection using executable assertions based on the natural constraints of the application.
This paper focuses on giving application-oriented fault tolerance a theoretical foundation by providing a mathematical model for the generation of executable assertions which detect faults in the presence of arbitrary failures. The mathematical model of choice was axiomatic program verification. A method was developed that translates a concurrent verification proof outline into an error-detecting concurrent program. This paper shows the application of the developed method to several applications.
Recommended Citation
Lutfiyya, Hanan; Schollmeyer, Martina; and McMillin, Bruce M., "Formal Generation of Executable Assertions for Application-Oriented Fault Tolerance" (1992). Computer Science Technical Reports. 19.
https://scholarsmine.mst.edu/comsci_techreports/19
Department(s)
Computer Science
Keywords and Phrases
Formal Methods; Fault Tolerance; Program Verification; Concurrent Systems; Algorithms
Report Number
CSC-92-15
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1992 University of Missouri--Rolla, All rights reserved.
Publication Date
05 Aug 1992
Comments
This work was supported in part by the National Science Foundation under Grant Numbers MIP-8909749 and CDA-8820714, and in part by the AMOCO Faculty Development Program.