Verifying Mutual Exclusion and Liveness Properties with Split Preconditions  

作　　者：AwadheshKumarSingh AnupKumarBandyopadhyay 

机构地区：[1]DepartmentofComputerEngineering,NationalInstituteofTechnology,Kurukshetra136119,India [2]DepartmentofElectronicsandTelecommunicationEngineering,JadavpurUniversity,Kolkata700032,India

出　　处：《Journal of Computer Science & Technology》2004年第6期795-802,共8页计算机科学技术学报（英文版）

摘　　要：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.

关 键 词：distributed algorithms state transition rule mutual exclusion weakest self-precondition weakest co-operation CORRECTNESS 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]