Formal Analysis of Suzuki&Kasami Distributed Mutual Exclusion Algorithm

Since parallel and distributed algorithms are subject to subtle errors that are unlikely to be detected in usual operation, only testing is not enough to reduce errors. Thus, it is necessary to formally analyze such algorithms in order to confirm that they have desirable properties. This paper describes the case study that Suzuki&Kasami distributed mutual exclusion algorithm is formally analyzed. In the case study, the algorithm has been modeled using UNITY-like models called observational transition systems (ots’s), the model has been described in CafeOBJ, and it has been verified that the algorithm is mutually exclusive and lockout free with the help of CafeOBJ system. In the verification that the algorithm is lockout free, we have found a hidden assumption necessary for the verification, which is not explicitly mentioned in the original paper written by Suzuki and Kasami.