Abstract
This paper presents a system for formally deriving executable assertions that can be evaluated in the faulty distributed computing environment. Since executable assertions for fault tolerance need to show that a program meets its specification and, since program verification is the process of formally showing that a program satisfies some particular properties with respect to its specification, we use program verification as a basis for derivation. It is well known that in the sequential computing environment the assertions from a program verification proof outline may be translated directly into executable assertions. However, due to the lack of global state information in a distributed program, this above translation will not work. The transformation system described in this paper addresses this problem by consistently communicating state information at run time relevant to the verification proof. The applicability of the transformation syste!Il is demonstrated through treatment of a distributed transaction scheduler.
Recommended Citation
Lutfiyya, Hanan; Schollmeyer, Martina; and McMillin, Bruce M., "Fault-Tolerant Distributed Database Lock Managers Formally Derived from Program Verification" (1992). Computer Science Technical Reports. 134.
https://scholarsmine.mst.edu/comsci_techreports/134
Department(s)
Computer Science
Keywords and Phrases
Executable Assertions, Formal Methods, Concurrent Program Verification, Fault Tolerance, Transformaation
Report Number
CSc-92-05
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
13 March, 1992
Comments
The first and second Authors are Graduate Students.
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.