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.
Lutfiyya, Hanan; Schollmeyer, Martina; and McMillin, Bruce M., "Formal Generation of Executable Assertions for Application-Oriented Fault Tolerance" (1992). Computer Science Technical Reports. 19.
Keywords and Phrases
Formal Methods; Fault Tolerance; Program Verification; Concurrent Systems; Algorithms
© 1992 University of Missouri--Rolla, All rights reserved.
05 Aug 1992