This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson's distributed mutual e...This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson's distributed mutual exclusion algorithm for two process has been considered. The proof of properties like, mutual exclusion, liveness, and lockout-freedom have also been presented. Keywords distributed algorithms - state transition rule - mutual exclusion - weakest self-precondition - weakest co-operation - correctness Regular PaperAwadhesh Kumar Singh received the B.E. degree in computer science & engineering from Gorakhpur University, Gorakhpur, India in 1988. He received the M.E. and Ph.D. (Engg) degrees in the same area from Jadavpur University, Kolkata, India. He is a faculty member in Computer Engineering Department, National Institute of Technology, Kurukshetra, India. His present research interest is distributed systems.Anup Kumar Bandyopadhyay received the B.E. (Tel.E.), M.E. (Tel.E.), and Ph.D. (Engg) degrees from Jadavpur University, Calcutta, India in 1968, 1970 and 1983, respectively. From 1970 to 1972 he worked with the Microwave Antenna System Engineering Group of the Indian Space Research Organization. In 1972 he joined the Department of Electronics and Telecommuication Engineering, Jadavpur University, where he is currently a professor. His research interests include computer communication networks and distributed systems.展开更多
文摘This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson's distributed mutual exclusion algorithm for two process has been considered. The proof of properties like, mutual exclusion, liveness, and lockout-freedom have also been presented. Keywords distributed algorithms - state transition rule - mutual exclusion - weakest self-precondition - weakest co-operation - correctness Regular PaperAwadhesh Kumar Singh received the B.E. degree in computer science & engineering from Gorakhpur University, Gorakhpur, India in 1988. He received the M.E. and Ph.D. (Engg) degrees in the same area from Jadavpur University, Kolkata, India. He is a faculty member in Computer Engineering Department, National Institute of Technology, Kurukshetra, India. His present research interest is distributed systems.Anup Kumar Bandyopadhyay received the B.E. (Tel.E.), M.E. (Tel.E.), and Ph.D. (Engg) degrees from Jadavpur University, Calcutta, India in 1968, 1970 and 1983, respectively. From 1970 to 1972 he worked with the Microwave Antenna System Engineering Group of the Indian Space Research Organization. In 1972 he joined the Department of Electronics and Telecommuication Engineering, Jadavpur University, where he is currently a professor. His research interests include computer communication networks and distributed systems.
