Abstract
Distributed database applications are a wide use of distributed systems. One of the major advantages of distributed database systems is the potential for achieving high availability in the presence of faults. Faults must be handled so that the system still operates or operates in a degraded mode. This paper focuses on being able to detect component errors which can lead to system failures in the scheduling part of the lock manager portion of the distributed database system by using embedded executable assertions. Changeling provides a systematic approach, based on the mathematical model of program verification, to deriving executable assertions that can be evaluated in the faulty distributed computing environment. A complete case study of the development of an error-detecting distributed scheduler, using Changeling, is presented in this paper.
Recommended Citation
Lutffiya, Hanan; McMillin, Bruce M.; and Su, Alan, "Formal Derivation of an Error-Detecting Distributed Data Scheduler using Changeling" (1992). Computer Science Technical Reports. 143.
https://scholarsmine.mst.edu/comsci_techreports/143
Department(s)
Computer Science
Keywords and Phrases
Distributed Databases, Executable Assertions, Formal Methods, Concurrent Program Verification, Fault Tolerance, Transformation, Changeling.
Report Number
CSc-92-14
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
15 September, 1992

Comments
The first and third Authors are Graduate Students.
1l1is work was supported in pa11 by the National Science Foundation under Grant Numbers MIP-8909749 and CDA-8820714, and in part by the University of Western Ontario.