Verification of HS leader election protocol using a mechanized framework

Verification of distributed system protocols either suffers from state-space explosion in composing the combined behavior of a number of identical participating processes or lacs in automated theorem proving technique to handle it. HS leader election protocol in a bidirectional synchronous ring is one such distributed system protocol whose verification also faces the same difficulties. A new mechanized verification framework proposed recently by the authors combines the tableau based theorem proving approach and model checking. It claims to have addressed the issues. In this paper authors have used this framework to verify the liveness property of HS Leader Election Protocol in a bidirectional synchronous ring to show that it can be effectively mechanized.