Abstract
A large number of published distributed deadlock detection/resolution algorithms are found to be incorrect because they have used informal approaches to prove the correctness of their algorithms. In this paper, we present a formal approach for the correctness proof and give an example of the proof. In this proposed approach, a formal model of distributed deadlock is presented with a local-time deadlock specification for correctness verification. With the formal model, we have an insight into the definition of deadlock in local views which is used to show the existence of a real deadlock. A rigorous proof to show the equivalence of local-time and global-time deadlock specifications is presented.
Recommended Citation
Li, Pei-yu and McMillin, Bruce, "Formal Verification of Distributed Deadlock Detection Algorithm using a Time-dependent Proof Technique" (1994). Computer Science Technical Reports. 155.
https://scholarsmine.mst.edu/comsci_techreports/155
Department(s)
Computer Science
Report Number
CSc-94-06
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1994 University of Missouri - Rolla, All rights reserved
Publication Date
11 February, 1994
Comments
The first Author is a Graduate Student