Verifying Mutual Exclusion and Liveness Properties with Split Preconditions

• 作 者: Awadhesh Kumar Singh Anup Kumar Bandyopadhyay
• 机 构: Department of Computer Engineering, National Institute of Technology, Kurukshetra 136119, India;Depa
• 出 处: 计算机科学技术学报（英文版）
• 发表日期: 2004年期
• 关键词: distributed algorithms state transition rule mutual exclusion weakest self-preco

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 Petersons 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.